PhD defended on Monday, October 13th 2014
Static analysis by abstract interpretation
Julien worked on static analysis by Abstract Interpretation, which is a commonly used technique to discover properties about a program (loop invariants, etc.). This technique computes an over-approximations of the set of possible states of the program. Julien’s topic was to refine this technique by using decision procedures (SMT-solving), in order to compute more precise invariants.
- How to compute worst-case execution time by optimization modulo theory and a clever encoding of program semantics. Henry, Julien and Asavoae, Mihail and Monniaux, David and Maiza, Claire (in SIGPLAN/SIGBED Conference on Languages, Compilers and Tools for Embedded Systems 2014, LCTES '14, 2014) [URL]
- Static Analysis by Abstract Interpretation and Decision Procedures. Henry, Julien (2014) [URL | PDF]
- PAGAI: a path sensitive static analyzer. Henry, Julien and Monniaux, David and Moy, Matthieu (in Tools for Automatic Program Analysis (TAPAS), 2012)
- Succinct Representations for Abstract Interpretation. Henry, Julien and Monniaux, David and Moy, Matthieu (in Static analysis (SAS), 2012)
- When the decreasing sequence fails. Halbwachs, Nicolas and Henry, Julien (in 19th International Static Analysis Symposium, SAS'12, 2012) [URL | PDF]