Julien Henry (Verimag): Improving static analysis with decision procedures
A widely-used approach to static program analysis is Abstract Interpretation, which consists in computing an over-approximation of the set of reachable program states, for any possible program execution. The main challenge is then to compute an approximation sufficiently precise to prove the desired properties (e.g. no division by zero, no arithmetic overflow etc). In this work, we propose several ways of using Satisfiability Modulo Theories to improve precision of the abstract interpretation framework. We present a static analyzer for C implementing these new methods, called PAGAI, that can use any SMT-solver supporting SMTLib2. Finally, we describe an interesting application of SMT to the estimation of Worst-Case Execution Time, which leads to formulas that are hard to solve by any production-grade solver based on DPLL(T). We show how a simple static analysis of the program dramatically helps the SMT solver to decide unsatisfiability faster in this particular case.