Static Analysis by Path Focusing
Program verification aims at statically discovering properties on programs,
such as the values that can take the different variables during execution.
Abstract Interpretation is a technique that computes an
over-approximation of the set of these values, since it is impossible to
compute the real set in general.
This report takes place in the many attempts to improve the precision of
static Analysis by Abstract Interpretation. It proposes a technique that
takes benefit of SMT-solving to obtain more precise results at reasonable
- 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]