Skip to main content
SpringerLink
Log in

Heaps and Data Structures: A Challenge for Automated Provers

  • Conference paper
Automated Deduction – CADE-23 (CADE 2011)

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

Included in the following conference series:

Abstract

Software verification is one of the most prominent application areas for automatic reasoning systems, but their potential improvement is limited by shortage of good benchmarks. Current benchmarks are usually large but shallow, require decision procedures, or have soundness problems. In contrast, we propose a family of benchmarks in first-order logic with equality which is scalable, relatively simple to understand, yet closely resembles difficult verification conditions stemming from real-world C code. Based on this benchmark, we present a detailed comparison of different heap encodings using a number of SMT solvers and ATPs. Our results led to a performance gain of an order of magnitude for the C code verifier VCC.

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. Armando, A., Bonacina, M.P., Ranise, S., Schulz, S.: New results on rewrite-based satisfiability procedures. ACM Transactions on Computational Logic 10(1) (2009)

    Google Scholar 

  2. Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: A modular reusable verifier for object-oriented programs. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 364–387. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  3. Barrett, C., Stump, A., Tinelli, C.: The Satisfiability Modulo Theories Library, SMT-LIB (2010), http://www.SMT-LIB.org

  4. Barrett, C.W., Tinelli, C.: CVC3. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 298–302. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  5. Bornat, R.: Proving pointer programs in Hoare Logic. In: Backhouse, R., Oliveira, J.N. (eds.) MPC 2000. LNCS, vol. 1837, pp. 102–126. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  6. Burstall, R.M.: Some techniques for proving correctness of programs which alter data structures. Machine Intelligence 7, 23–50 (1972)

    MATH  Google Scholar 

  7. Cartwright, R., Oppen, D.: The logic of aliasing. Acta Informatica 15, 365–384 (1981)

    Article  MATH  MathSciNet  Google Scholar 

  8. Cohen, E., Dahlweid, M., Hillebrand, M., Leinenbach, D., Moskal, M., Santen, T., Schulte, W., Tobies, S.: VCC: A practical system for verifying concurrent C. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 23–42. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  9. Cohen, E., Moskal, M., Tobies, S., Schulte, W.: A precise yet efficient memory model for C. ENTCS 254, 85–103 (2009)

    Google Scholar 

  10. Condit, J., Hackett, B., Lahiri, S.K., Qadeer, S.: Unifying type checking and property checking for low-level code. In: POPL, pp. 302–314. ACM, New York (2009)

    Google Scholar 

  11. de Moura, L., Bjørner, N.S.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  12. de Moura, L.M., Bjørner, N.: Generalized, efficient array decision procedures. In: Formal Methods in Computer-Aided Design, pp. 45–52. IEEE, Los Alamitos (2009)

    Google Scholar 

  13. Dutertre, B., de Moura, L.: The Yices SMT solver (2006), http://yices.csl.sri.com/tool-paper.pdf

  14. Filliâtre, J.-C.: Why: a multi-language multi-prover verification tool. Research Report 1366, LRI, Université Paris Sud (March 2003)

    Google Scholar 

  15. Hoare, C.A.R.: The verifying compiler: A grand challenge for computing research. Journal of the ACM 50(1), 63–69 (2003)

    Article  MATH  Google Scholar 

  16. James, P., Chalin, P.: Faster and more complete extended static checking for the Java Modeling Language. Journal of Automated Reasoning 44, 145–174 (2010)

    Article  MATH  Google Scholar 

  17. Kuncak, V.: Modular Data Structure Verification. PhD thesis, EECS Department, Massachusetts Institute of Technology (February 2007)

    Google Scholar 

  18. Leinenbach, D., Santen, T.: Verifying the microsoft hyper-V hypervisor with VCC. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol. 5850, pp. 806–809. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  19. Leino, K.R.M.: Dafny: An automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR-16 2010. LNCS, vol. 6355, pp. 348–370. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  20. Leino, K.R.M., Moskal, M.: VACID-0: Verification of Ample Correctness of Invariants of Data-structures. In: VSTTE (2010)

    Google Scholar 

  21. McCune, W.: OTTER 3.3 Reference Manual. Mathematics and Computer Science Division, Argonne National Laboratory, Technical Memorandum No. 263 (2003)

    Google Scholar 

  22. Moskal, M.: Fx7 or in software, it is all about quantifiers. Satisfiability Modulo Theories Competition (2007)

    Google Scholar 

  23. Moskal, M.: Programming with triggers. In: SMT 2009, pp. 20–29. ACM, New York (2009)

    Google Scholar 

  24. Nelson, G.: Techniques for program verification. Technical Report CSL-81-10, Xerox PARC (1981)

    Google Scholar 

  25. Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL–Isabelle/HOL – A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002)

    MATH  Google Scholar 

  26. Riazanov, A., Voronkov, A.: The design and implementation of Vampire. AI Comm. 15(2-3), 91–110 (2002)

    MATH  Google Scholar 

  27. Schulz, S.: System description: E 0.81. In: Basin, D., Rusinowitch, M. (eds.) IJCAR 2004. LNCS (LNAI), vol. 3097, pp. 223–228. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  28. Sutcliffe, G.: The TPTP problem library and associated infrastructure. Journal of Automated Reasoning 43(4), 337–362 (2009)

    Article  MATH  Google Scholar 

  29. Veroff, R.: Using hints to increase the effectiveness of an automated reasoning program: Case studies. Journal of Automated Reasoning 16, 223–239 (1996)

    Article  MATH  MathSciNet  Google Scholar 

  30. Weidenbach, C., Dimova, D., Fietzke, A., Kumar, R., Suda, M., Wischnewski, P.: SPASS version 3.5. In: Schmidt, R.A. (ed.) CADE-22. LNCS, vol. 5663, pp. 140–145. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  31. Zee, K., Kuncak, V., Rinard, M.C.: Full functional verification of linked data structures. In: Programming Language Design and Implementation, pp. 349–361. ACM, New York (2008)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Technische Universität, München, Germany

    Sascha Böhme

  2. Microsoft Research, Redmond, United States

    Michał Moskal

Authors
  1. Sascha Böhme
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Michał Moskal
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Microsoft Research, One Microsoft Way, 98052-6399, Redmond, WA, USA

    Nikolaj Bjørner

  2. Max-Planck-Institut für Informatik, Campus E 1.4, 66123, Saarbrücken, Germany

    Viorica Sofronie-Stokkermans

Rights and permissions

Reprints and permissions

Copyright information

© 2011 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Böhme, S., Moskal, M. (2011). Heaps and Data Structures: A Challenge for Automated Provers. In: Bjørner, N., Sofronie-Stokkermans, V. (eds) Automated Deduction – CADE-23. CADE 2011. Lecture Notes in Computer Science(), vol 6803. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-22438-6_15

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-22438-6_15

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-22437-9

  • Online ISBN: 978-3-642-22438-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation