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

References in zbMATH (referenced in 4 articles , 1 standard article )

Showing results 1 to 4 of 4.
Sorted by year (citations)

  1. Hoenicke, Jochen; Schindler, Tanja: Efficient interpolation for the theory of arrays (2018)
  2. Komuravelli, Anvesh; Gurfinkel, Arie; Chaki, Sagar: SMT-based model checking for recursive programs (2016)
  3. D’Silva, Vijay; Urban, Caterina: Conflict-driven conditional termination (2015)
  4. Heizmann, Matthias; Christ, Jürgen; Dietsch, Daniel; Ermis, Evren; Hoenicke, Jochen; Lindenmann, Markus; Nutz, Alexander; Schilling, Christian; Podelski, Andreas: Ultimate automizer with smtinterpol. (Competition contribution) (2013) ioport