Ultimate kojak. Ultimate Kojak is a symbolic software model checker for C programs. It is based on CEGAR and Craig interpolation. The basic algorithm, described in an earlier work , was extended to be able to deal with recursive programs using nested word automata and nested (tree) interpolants.
References in zbMATH (referenced in 4 articles , 1 standard article )
Showing results 1 to 4 of 4.
- Beyer, Dirk; Gulwani, Sumit; Schmidt, David A.: Combining model checking and data-flow analysis (2018)
- Hoenicke, Jochen; Schindler, Tanja: Efficient interpolation for the theory of arrays (2018)
- Dietsch, Daniel; Heizmann, Matthias; Langenfeld, Vincent; Podelski, Andreas: Fairness modulo theory: a new approach to LTL software model checking (2015)
- Ermis, Evren; Nutz, Alexander; Dietsch, Daniel; Hoenicke, Jochen; Podelski, Andreas: Ultimate kojak. (Competition contribution) (2014) ioport