Ultimate Automizer with Unsatisfiable Cores - (Competition Contribution).
Matthias Heizmann, Jürgen Christ, Daniel Dietsch, Jochen Hoenicke, Markus Lindenmann, Betim Musa, Christian Schilling, Stefan Wissert, Andreas Podelski · Tools and Algorithms for Construction and Analysis of Systems · 2014
Ultimate Automizer is an automatic software verification tool for C programs. This tool is a prototype implementation of an automata-theoretic approach that allows a modular verification of pro- grams. Furthermore, this is the first implementation of a novel interpola- tion technique where interpolants are not obtained from an interpolating theorem prover but from a combination of a live variable analysis, inter- procedural predicate transformers and unsatisfiable cores.