Traces, Interpolants, and Automata: a New Approach to Automatic Software Verification

Matthias Heizmann (University of Freiburg)

When: May 11, 2pm

Where: room C417


We will cover the principles underlying a recent approach to the verification of different classes of correctness properties (safety, termination) for programs. The approach is based on a new view to programs where the control flow graph is considered as an automaton. The alphabet of this automaton are the program's statements. The language of this automaton are the traces of the program. We will use automata-theoretic operations to decompose a program into sets of traces and prove correctness for each set of traces individually. For the verification of recursive programs we use nested word automata and for termination analysis we use the B├╝chi acceptance condition.