Ultimate Automizer with Array Interpolation

(Competition Contribution)
  • Matthias Heizmann
  • Daniel Dietsch
  • Jan Leike
  • Betim Musa
  • Andreas Podelski
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9035)


Ultimate Automizer is a software verification tool that is able to analyze reachability of an error label, memory safety, and termination of C programs. For all three tasks, our tool follows an automata-based approach where interpolation is used to compute proofs for traces. The interpolants are generated via a new scheme that requires only the post operator, unsatisfiable cores and live variable analysis. This new scheme enables our tool to use the SMT theory of arrays in combination with interpolation.


Python Script Error Trace Sample Trace Software Model Check Error Label 
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.
    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
  2. 2.
    Heizmann, M., Hoenicke, J., Podelski, A.: Nested interpolants. In: Hermenegildo, M.V., Palsberg, J. (eds.) POPL, pp. 471–482. ACM (2010)Google Scholar
  3. 3.
    Heizmann, M., Hoenicke, J., Podelski, A.: Software model checking for people who love automata. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 36–52. Springer, Heidelberg (2013)Google Scholar
  4. 4.
    Heizmann, M., Hoenicke, J., Podelski, A.: Termination analysis by learning terminating programs. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 797–813. Springer, Heidelberg (2014)Google Scholar
  5. 5.
    Leike, J., Heizmann, M.: Geometric series as nontermination arguments for linear lasso programs. In: WST, pp. 55–59 (2014)Google Scholar
  6. 6.
    Leike, J., Heizmann, M.: Ranking templates for linear loops. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014 (ETAPS). LNCS, vol. 8413, pp. 172–186. Springer, Heidelberg (2014)Google Scholar
  7. 7.
    Leino, K.R.M.: This is Boogie 2. Manuscript working draft. Microsoft Research, Redmond (June 2008),
  8. 8.
    Musa, B.: Trace abstraction with unsatisfiable cores. Bachelor’s thesis, University of Freiburg, Germany (2013)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2015

Authors and Affiliations

  • Matthias Heizmann
    • 1
  • Daniel Dietsch
    • 1
  • Jan Leike
    • 2
  • Betim Musa
    • 1
  • Andreas Podelski
    • 1
  1. 1.University of FreiburgFreiburgGermany
  2. 2.The Australian National UniversityCanberraAustralia

Personalised recommendations