Ultimate Automizer

Ultimate automizer with smtinterpol. (Competition contribution) Ultimate automizer is an automatic software verification tool for C programs. This tool is the first implementation of trace abstraction, which is an automata-theoretic approach to software verification. The implemented algorithm uses nested interpolants in its interprocedural program analysis. The interpolating SMT solver SMTInterpol is used to compute Craig interpolants.

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element