Ph.D

Group : Verification of Algorithms, Languages and Systems

*Random based testing of C program*
Starts on 01/10/2012

Advisor : WOLFF, Burkhart

**Funding :**
**Affiliation :** Université Paris-Sud

**Laboratory :** LRI Fortesse

**Defended** on 30/01/2017, committee :

Directeur de thèse :

- M. Burkhart Wolff, Professeur, Université Paris-Sud, LRI

Co-encadrants :

- M. Frédéric Voisin, Maître de conférence, Université Paris-Sud

- Mme Marie-Claude Gaudel, Professeur émérite, Université Paris-Sud

- Mme Sandrine Blazy, Professeur, Université Rennes 1,

- Mme Lydie du Bousquet, Professeur, Université Joseph Fournier, Grenoble,

- M. Alain Denise, Professeur, Université Paris-Sud,

- M. François Laroussinie, Professeur, Université Paris-Diderot,

- M. Jean-Yves Pierron, Ingénieur-chercheur, CEA-LIST

**Research activities :**
- Formal Model-Based Testing

**Abstract :**
A number of program analysis techniques are based on a graphical

representation of the program called the Control Flow Graph (CFG). A CFG

is a compact representation of a program's behavior: each possible

execution of the program is represented by exactly one path in the CFG.

The inverse property is not true: not every path of the CFG represents

an actual execution of the program. Such paths are said to be infeasible.

In general, the infeasible paths largely outnumber the feasible ones,

even in simple programs. As a result, analysis techniques based on

CFG's are usually negatively impacted by the existence of infeasible paths.

In this thesis, we present a conceptual algorithm that builds better approximations

of the set of feasible paths. Our work is based on a progressive unfolding of the CFG

by symbolic execution techniques and the use of constraint solving for

detecting infeasible paths. When programs contain loops, in which cases

the unfolding of all paths in its CFG would yield an infinite symbolic execution tree,

we introduce abstractions and subsumptions to turn back this potentially infinite

tree into a finite graph.

We introduce the theoretical concepts of our approach by a specific graph representation and five

transformations on it. We provide a complete formalization in Isabelle/HOL of both graph

structures and transformations in order to establish the main correctness theorems.

The formalisation is turned into a prototype implementing the five transformations

complemented with heuristics for their control. Finally, we present various experiments

performed with our prototype and the associated results.