It is known since Alan Turing that program analysis is undecidable except for very constrained classes of programs. Automated program analysis methods work around this major difficulty in two major ways.
One is to over-approximate the set of behaviors of the program by a simpler set. For instance, instead of tracking the precise set of values that the program variables may have at a given program location, one can track one interval of variation per variable. This approach generalizes to a theory of approximation of program semantics known as abstract interpretation.
Another is to consider finite execution traces and to convert the problem of deciding whether there exists some trace matching some property to the satisfiability of a first-order logical formula (typically over a combination of arithmetic and arrays). Depending on the class of formulas being considered, such problems are decidable but expensive (NP-hard) or even undecidable.
The PACSS team researches new approaches in abstract interpretation, decision procedures and combinations thereof, particularly within the STATOR project.
Faculty involved
- Nicolas Halbwachs
- David Monniaux
