Skip to main content

Traces, interpolants, and automata : Ultimate Automizer's approach to software verification

Matthias Heizmann ( University of Freiburg, Germany )

In this talk, we will see the approach to automatic software
verification that is implemented in the Ultimate Automizer tool.  The
approach is based on a new view to programs.  In this new view, the
focus lies not on program states, instead the focus lies on sequences of
statements, which we call traces.  We view a program as an automaton
whose alphabet consists of the program’s  statements.  Hence, each
program defines a set of traces and we can apply automata-theoretic
operations to programs.  Ultimate Automizer uses this connection between
programs and sets of traces to decompose a program, to prove correctness
of the components, and to compose these correctness proofs to a
correctness proof for the program.



Share this: