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

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-Saclay
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.

Ph.D. dissertations & Faculty habilitations


The topic of this habilitation is the study of very small data visualizations, micro visualizations, in display contexts that can only dedicate minimal rendering space for data representations. For several years, together with my collaborators, I have been studying human perception, interaction, and analysis with micro visualizations in multiple contexts. In this document I bring together three of my research streams related to micro visualizations: data glyphs, where my joint research focused on studying the perception of small-multiple micro visualizations, word-scale visualizations, where my joint research focused on small visualizations embedded in text-documents, and small mobile data visualizations for smartwatches or fitness trackers. I consider these types of small visualizations together under the umbrella term ``micro visualizations.'' Micro visualizations are useful in multiple visualization contexts and I have been working towards a better understanding of the complexities involved in designing and using micro visualizations. Here, I define the term micro visualization, summarize my own and other past research and design guidelines and outline several design spaces for different types of micro visualizations based on some of the work I was involved in since my PhD.