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

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.