Français Anglais
Accueil Annuaire Plan du site
Home > Research results > Dissertations & habilitations
Research results
Ph.D de

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.