Skip to main content
SpringerLink
Log in

Definability of Accelerated Relations in a Theory of Arrays and Its Applications

  • Conference paper
Book cover Frontiers of Combining Systems (FroCoS 2013)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 8152))

Included in the following conference series:

Abstract

For some classes of guarded ground assignments for arrays, we show that accelerations (i.e. transitive closures) are definable in the theory of arrays via ∃ * ∀ *-first order formulae. We apply this result to model checking of unbounded array programs, where the computation of such accelerations can be used to prevent divergence of reachability analysis. To cope with nested quantifiers introduced by acceleration preprocessing, we use simple instantiation and refinement strategies during backward search analysis. Our new acceleration technique and abstraction/refinement loops are mutually beneficial: experiments conducted with the SMT-based model checker mcmt attest the effectiveness of our approach where acceleration and abstraction/refinement technologies fail if applied alone.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Abdulla, P.A., Delzanno, G., Ben Henda, N., Rezine, A.: Regular model checking without transducers (On efficient verification of parameterized systems). In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 721–736. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  2. Abdulla, P.A., Delzanno, G., Rezine, A.: Parameterized verification of infinite-state processes with global conditions. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 145–157. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  3. Alberti, F., Bruttomesso, R., Ghilardi, S., Ranise, S., Sharygina, N.: Lazy Abstraction with Interpolants for Arrays. In: Bjørner, N., Voronkov, A. (eds.) LPAR-18. LNCS, vol. 7180, pp. 46–61. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  4. Alberti, F., Bruttomesso, R., Ghilardi, S., Ranise, S., Sharygina, N.: SAFARI: SMT-Based Abstraction for Arrays with Interpolants. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 679–685. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  5. Alberti, F., Ghilardi, S., Pagani, E., Ranise, S., Rossi, G.P.: Universal Guards, Relativization of Quantifiers, and Failure Models in Model Checking Modulo Theories. JSAT, 29–61 (2012)

    Google Scholar 

  6. Alberti, F., Ghilardi, S., Sharygina, N.: Tackling divergence: abstraction and acceleration in array programs. Technical Report 2012/01, University of Lugano (October 2012)

    Google Scholar 

  7. Ball, T., Rajamani, S.K.: The SLAM toolkit. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 260–264. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  8. Barrett, C., Stump, A., Tinelli, C.: The SMT-LIB Standard: Version 2.0 (2010), http://www.smt-lib.org

  9. Behrmann, G., Bengtsson, J., David, A., Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL implementation secrets. In: Damm, W., Olderog, E.-R. (eds.) FTRTFT 2002. LNCS, vol. 2469, pp. 3–22. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  10. Beyer, D., Henzinger, T.A., Majumdar, R., Rybalchenko, A.: Path invariants. In: PLDI, pp. 300–309 (2007)

    Google Scholar 

  11. Borralleras, C., Lucas, S., Oliveras, A., Rodríguez-Carbonell, E., Rubio, A.: SAT modulo linear arithmetic for solving polynomial constraints. J. Autom. Reasoning 48(1), 107–131 (2012)

    Article  MATH  Google Scholar 

  12. Bozga, M., Gîrlea, C., Iosif, R.: Iterating octagons. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 337–351. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  13. Bozga, M., Habermehl, P., Iosif, R., Konečný, F., Vojnar, T.: Automatic verification of integer array programs. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 157–172. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  14. Bozga, M., Iosif, R., Konečný, F.: Fast acceleration of ultimately periodic relations. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 227–242. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  15. Bozga, M., Iosif, R., Lakhnech, Y.: Flat parametric counter automata. Fundam. Inform. 91(2), 275–303 (2009)

    MathSciNet  MATH  Google Scholar 

  16. 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)

    Chapter  Google Scholar 

  17. Caniart, N., Fleury, E., Leroux, J., Zeitoun, M.: Accelerating interpolation-based model-checking. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 428–442. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  18. Cimatti, A., Griggio, A., Sebastiani, R.: Efficient generation of Craig interpolants in satisfiability modulo theories. ACM Trans. Comput. Log. 12(1), 7 (2010)

    Article  MathSciNet  Google Scholar 

  19. Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-Guided Abstraction Refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154–169. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  20. Comon, H., Jurski, Y.: Multiple counters automata, safety analysis and presburger arithmetic. In: Vardi, M.Y. (ed.) CAV 1998. LNCS, vol. 1427, pp. 268–279. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  21. Finkel, A., Leroux, J.: How to compose presburger-accelerations: Applications to broadcast protocols. In: Agrawal, M., Seth, A.K. (eds.) FSTTCS 2002. LNCS, vol. 2556, pp. 145–156. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  22. Flanagan, C., Qadeer, S.: Predicate abstraction for software verification. In: POPL, pp. 191–202 (2002)

    Google Scholar 

  23. Ge, Y., de Moura, L.: Complete instantiation for quantified formulas in Satisfiabiliby Modulo Theories. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 306–320. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  24. Ghilardi, S., Ranise, S.: MCMT: A Model Checker Modulo Theories. In: Giesl, J., Hähnle, R. (eds.) IJCAR 2010. LNCS, vol. 6173, pp. 22–29. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  25. Graf, S., Saïdi, H.: Construction of Abstract State Graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72–83. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  26. Hendriks, M., Larsen, K.G.: Exact acceleration of real-time model checking. Electr. Notes Theor. Comput. Sci. 65(6), 120–139 (2002)

    Article  Google Scholar 

  27. Hojjat, H., Iosif, R., Konečný, F., Kuncak, V., Rümmer, P.: Accelerating interpolants. In: Chakraborty, S., Mukund, M. (eds.) ATVA 2012. LNCS, vol. 7561, pp. 187–202. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  28. Jhala, R., McMillan, K.L.: Array Abstractions from Proofs. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 193–206. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  29. Kovács, L., Voronkov, A.: Interpolation and Symbol Elimination. In: Schmidt, R.A. (ed.) CADE 2009. LNCS, vol. 5663, pp. 199–213. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  30. Larraz, D., Rodríguez-Carbonell, E., Rubio, A.: SMT-based array invariant generation. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 169–188. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  31. McMillan, K.L.: Lazy Abstraction with Interpolants. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 123–136. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  32. McMillan, K.L.: 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)

    Chapter  Google Scholar 

  33. Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Transaction on Programming Languages and Systems 1(2), 245–257 (1979)

    Article  MATH  Google Scholar 

  34. Seghir, M.N., Podelski, A., Wies, T.: Abstraction Refinement for Quantified Array Assertions. In: Palsberg, J., Su, Z. (eds.) SAS 2009. LNCS, vol. 5673, pp. 3–18. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  35. Srivastava, S., Gulwani, S.: Program Verification using Templates over Predicate Abstraction. In: PLDI (2009)

    Google Scholar 

  36. Tinelli, C., Harandi, M.T.: A new correctness proof of the Nelson-Oppen combination procedure. In: Proc. of FroCoS 1996, pp. 103–119. Kluwer (1996)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Formal Verification Lab, University of Lugano, Lugano, Switzerland

    Francesco Alberti & Natasha Sharygina

  2. Università degli Studi di Milano, Milan, Italy

    Silvio Ghilardi

Authors
  1. Francesco Alberti
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Silvio Ghilardi
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Natasha Sharygina
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. LORIA, Inria Nancy Grand Est, Université de Lorraine, 615 rue du Jardin Botanique, 54602, Villers-les-Nancy, France

    Pascal Fontaine

  2. LORIA, Inria Nancy Grand Est, 615 rue du Jardin Botanique, 54602, Villers-lès-Nancy, France

    Christophe Ringeissen

  3. School of Computer Science, The University of Manchester, Oxford Rd, Kilburn Building, M13 9PL, Manchester, UK

    Renate A. Schmidt

Rights and permissions

Reprints and permissions

Copyright information

© 2013 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Alberti, F., Ghilardi, S., Sharygina, N. (2013). Definability of Accelerated Relations in a Theory of Arrays and Its Applications. In: Fontaine, P., Ringeissen, C., Schmidt, R.A. (eds) Frontiers of Combining Systems. FroCoS 2013. Lecture Notes in Computer Science(), vol 8152. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-40885-4_3

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-40885-4_3

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-40884-7

  • Online ISBN: 978-3-642-40885-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation