Automatic Verification of Integer Array Programs

  • Marius Bozga
  • Peter Habermehl
  • Radu Iosif
  • Filip Konečný
  • Tomáš Vojnar
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5643)


We provide a verification technique for a class of programs working on integer arrays of finite, but not a priori bounded length. We use the logic of integer arrays SIL [13] to specify pre- and post-conditions of programs and their parts. Effects of non-looping parts of code are computed syntactically on the level of SIL. Loop pre-conditions derived during the computation in SIL are converted into counter automata (CA). Loops are automatically translated—purely on the syntactical level—to transducers. Pre-condition CA and transducers are composed, and the composition over-approximated by flat automata with difference bound constraints, which are next converted back into SIL formulae, thus inferring post-conditions of the loops. Finally, validity of post-conditions specified by the user in SIL may be checked as entailment is decidable for SIL.


Scalar Variable Transitive Closure Conditional Statement Array Variable Boolean Combination 
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., Henzinger, T.A., Majumdar, R., Rybalchenko, A.: Invariant Synthesis for Combined Theories. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol. 4349, pp. 378–394. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  2. 2.
    Beyer, D., Henzinger, T.A., Majumdar, R., Rybalchenko, A.: Path Invariants. In: Proc. of PLDI 2007, ACM SIGPLAN (2007)Google Scholar
  3. 3.
    Bouajjani, A., Habermehl, P., Jurski, Y., Sighireanu, M.: Rewriting Systems with Data: A Framework for Reasoning about Systems with Unbounded Structures over Infinite Data Domains. In: Csuhaj-Varjú, E., Ésik, Z. (eds.) FCT 2007. LNCS, vol. 4639, pp. 1–22. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  4. 4.
    Bozga, M., Habermehl, P., Iosif, R., Konečný, F., Vojnar, T.: Automatic Verification of Integer Array Programs. Technical Report TR-2009-2, Verimag, Grenoble, France (2009)Google Scholar
  5. 5.
    Bozga, M., Iosif, R., Lakhnech, Y.: Flat Parametric Counter Automata. In: Bugliesi, M., Preneel, B., Sassone, V., Wegener, I. (eds.) ICALP 2006. LNCS, vol. 4052, pp. 577–588. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  6. 6.
    Bradley, A.R., Manna, Z., Sipma, H.B.: What’s Decidable About Arrays? In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 427–442. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  7. 7.
    Comon, H., Jurski, Y.: Multiple Counters Automata, Safety Analysis and Presburger Arithmetic. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol. 1427. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  8. 8.
    Flanagan, C., Qadeer, S.: Predicate Abstraction for Software Verification. In: Proc. of POPL 2002. ACM, New York (2002)Google Scholar
  9. 9.
    Ghilardi, S., Nicolini, E., Ranise, S., Zucchelli, D.: Decision Procedures for Extensions of the Theory of Arrays. Annals of Mathematics and Artificial Intelligence 50 (2007)Google Scholar
  10. 10.
    Ghilardi, S., Nicolini, E., Ranise, S., Zucchelli, D.: Towards SMT Model Checking of Array-based Systems. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS, vol. 5195, pp. 67–82. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  11. 11.
    Gopan, D., Reps, T.W., Sagiv, S.: A Framework for Numeric Analysis of Array Operations. In: POPL 2005. ACM, New York (2005)Google Scholar
  12. 12.
    Gulwani, S., McCloskey, B., Tiwari, A.: Lifting Abstract Interpreters to Quantified Logical Domains. In: POPL 2008. ACM, New York (2008)Google Scholar
  13. 13.
    Habermehl, P., Iosif, R., Vojnar, T.: A Logic of Singly Indexed Arrays. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol. 5330, pp. 558–573. Springer, Heidelberg (2008)Google Scholar
  14. 14.
    Habermehl, P., Iosif, R., Vojnar, T.: What Else is Decidable about Integer Arrays? In: Amadio, R. (ed.) FOSSACS 2008. LNCS, vol. 4962, pp. 474–489. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  15. 15.
    Halbwachs, N., Péron, M.: Discovering Properties about Arrays in Simple Programs. In: Proc. of PLDI 2008. ACM, New York (2008)Google Scholar
  16. 16.
    Jhala, R., McMillan, K.: Array Abstractions from Proofs. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 193–206. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  17. 17.
    Kovács, L., Voronkov, A.: Finding Loop Invariants for Programs over Arrays Using a Theorem Prover. In: Chechik, M., Wirsing, M. (eds.) FASE 2009. LNCS, vol. 5503, pp. 470–486. Springer, Heidelberg (2009)Google Scholar
  18. 18.
    Lahiri, S.K., Bryant, R.E.: Indexed Predicate Discovery for Unbounded System Verification. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 135–147. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  19. 19.
    Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems. Springer, Heidelberg (1992)CrossRefzbMATHGoogle Scholar
  20. 20.
    McMillan, K.: Quantified Invariant Generation Using an Interpolating Saturation Prover. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 413–427. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  21. 21.
    Stump, A., Barrett, C.W., Dill, D.L., Levitt, J.R.: A Decision Procedure for an Extensional Theory of Arrays. In: Proc. of LICS 2001. IEEE Computer Society, Los Alamitos (2001)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2009

Authors and Affiliations

  • Marius Bozga
    • 1
  • Peter Habermehl
    • 2
  • Radu Iosif
    • 1
  • Filip Konečný
    • 1
    • 3
  • Tomáš Vojnar
    • 3
  1. 1.VERIMAG, CNRSGièresFrance
  2. 2.LIAFAParis 13France
  3. 3.FIT BUTBrnoCzech Republic

Personalised recommendations