Ultimate Kojak

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 [1], 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.
Sorted by year (citations)

  1. Beyer, Dirk; Gulwani, Sumit; Schmidt, David A.: Combining model checking and data-flow analysis (2018)
  2. Hoenicke, Jochen; Schindler, Tanja: Efficient interpolation for the theory of arrays (2018)
  3. Dietsch, Daniel; Heizmann, Matthias; Langenfeld, Vincent; Podelski, Andreas: Fairness modulo theory: a new approach to LTL software model checking (2015)
  4. Ermis, Evren; Nutz, Alexander; Dietsch, Daniel; Hoenicke, Jochen; Podelski, Andreas: Ultimate kojak. (Competition contribution) (2014) ioport