Trace Abstraction in Ultimate Automizer

We present an approach to program verification that is embodied by the tool Ultimate Automizer. Ultimate Automizer exploits the idea of behavioral decomposition: we can decompose the set of behaviors of a given program (whose correctness we want to prove) according to sets of behaviors for which we already have a proof. We obtain proven behaviors by constructing auxiliary programs from traces (i.e., sequences of statements) of the input program. In its simplest form, an auxiliary program is just one trace, i.e., a straight-line program. At the same time, a trace is a word over a finite alphabet, which can be accepted by an automaton. Just as we ask whether a word has an accepting run, we can ask whether a trace has a correctness proof, e.g. in the form of a set of Hoare triples. From such a set of Hoare triples, we can construct an automaton that recognizes all words over the alphabet of program statements that are correct because of this proof. Such an automaton is a program whose set of behaviors covers a non-empty subset of behaviors of our input program. We repeatedly construct such programs from proofs until the constructed programs together cover all possible behaviors of the input program. The two crucial steps of the algorithm are the covering check and the construction of a set of Hoare triples. Covering utilizes many algorithms for automata, e.g. inclusion, difference and minimization. Construction and extension of Hoare triple sets can be performed by Craig interpolation, abstract interpretation, and a combination of strongest post with unsatisfiable cores and dataflow analysis. Ultimate Automizer and other tools of the Ultimate family apply this approach to a wide range of verification problems, most prominently checking safety and termination of sequential C programs with recursive procedures, but also treating liveness properties or multi-threaded programs with possibly unboundedly many threads.