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
References in zbMATH (referenced in 4 articles , 1 standard article )
Showing results 1 to 4 of 4.
- Hoenicke, Jochen; Schindler, Tanja: Efficient interpolation for the theory of arrays (2018)
- Komuravelli, Anvesh; Gurfinkel, Arie; Chaki, Sagar: SMT-based model checking for recursive programs (2016)
- D’Silva, Vijay; Urban, Caterina: Conflict-driven conditional termination (2015)
- 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