[pl-seminar] PL-Seminar - Julien Henry - Thursday 10/30 4:00pm Room 4310

[Julien Henry <jhenry@xxxxxxxxxxx>]

Hello, 

I will be giving a PL seminar tomorrow at 4:00pm in the room 4310. 

Abstract:

Static program analysis aims at automatically determining whether a program satisfies some particular properties. For this purpose, abstract interpretation is a framework that enables the computation of invariants, i.e. properties on the variables that always hold for any program execution. The precision of these invariants depends on many parameters, in particular the abstract domain, and the iteration strategy for computing these invariants. We propose to use Satisfiability Modulo Theories to guide the fixpoint computation, that enhance the overall precision of the analysis.

We then describe an application of static analysis and SMT to the estimation of program worst-case execution time (WCET). We first present how to express WCET as an optimization modulo theory problem, and show that natural encodings into SMT yield formulas intractable for all current production-grade solvers. We propose an efficient way to considerably reduce the computation time of the SMT-solvers by conjoining to the formulas well chosen summaries of program portions obtained by static analysis.

We finally describe Pagai, a new static analyzer working over the LLVM compiler infrastructure, which computes numerical inductive invariants using several state of the art techniques. We provide experimental results on the Software Verification Competition (SV-COMP).