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-Saclay
Laboratory : LRI Fortesse

Defended on 30/01/2017, committee :

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.

CAUSAL LEARNING FOR DIAGNOSTIC SUPPORT


CAUSAL UNCERTAINTY QUANTIFICATION UNDER PARTIAL KNOWLEDGE AND LOW DATA REGIMES


MICRO VISUALIZATIONS: DESIGN AND ANALYSIS OF VISUALIZATIONS FOR SMALL DISPLAY SPACES
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.