ULTIMATE KOJAK with Memory Safety Checks

(Competition Contribution)
  • Alexander NutzEmail author
  • Daniel Dietsch
  • Mostafa Mahmoud Mohamed
  • Andreas Podelski
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9035)


Ultimate Kojak is a symbolic software model checker implemented in the Ultimate framework. It follows the CEGAR approach and uses Craig interpolants to refine an overapproximation of the program until it can either prove safety or has found a real counterexample.

This year’s version features a new refinement algorithm, a precise treatment of heap memory, which allows us to deal with pointer aliasing and to participate in the memsafety category, and an improved interpolants generator.


Memory Model Program Graph Error Path Software Model Checker Heap Memory 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 1.
    Beyer, D., Cimatti, A., Griggio, A., Keremoglu, M.E., Sebastiani, R.: Software model checking via large-block encoding. In: FMCAD, pp. 25–32. IEEE (2009)Google Scholar
  2. 2.
    Christ, J., Hoenicke, J., Nutz, A.: SMTInterpol: An interpolating SMT solver. In: Donaldson, A., Parker, D. (eds.) SPIN 2012. LNCS, vol. 7385, pp. 248–254. Springer, Heidelberg (2012)Google Scholar
  3. 3.
    Ermis, E., Hoenicke, J., Podelski, A.: Splitting via interpolants. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol. 7148, pp. 186–201. Springer, Heidelberg (2012)Google Scholar
  4. 4.
    Heizmann, M., Hoenicke, J., Podelski, A.: Nested interpolants. In: Hermenegildo, M.V., Palsberg, J. (eds.) POPL, pp. 471–482. ACM (2010)Google Scholar
  5. 5.
    Leino, K.R.M.: This is Boogie 2. Manuscript working draft. Microsoft Research, Redmond (2008), Google Scholar
  6. 6.
    Musa, B.: Trace abstraction with unsatisfiable cores. Bachelor’s thesis, University of Freiburg, Germany (2013)Google Scholar
  7. 7.
    Nutz, A.: Impulse: a new interpolating software model checker. Master’s thesis, University of Freiburg, Germany (2011)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2015

Authors and Affiliations

  • Alexander Nutz
    • 1
    Email author
  • Daniel Dietsch
    • 1
  • Mostafa Mahmoud Mohamed
    • 1
  • Andreas Podelski
    • 1
  1. 1.University of FreiburgFreiburgGermany

Personalised recommendations