Skip to main content
SpringerLink
Log in

Deciding Functional Lists with Sublist Sets

  • Conference paper
Verified Software: Theories, Tools, Experiments (VSTTE 2012)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 7152))

Abstract

Motivated by the problem of deciding verification conditions for the verification of functional programs, we present new decision procedures for automated reasoning about functional lists. We first show how to decide in NP the satisfiability problem for logical constraints containing equality, constructor, selectors, as well as the transitive sublist relation. We then extend this class of constraints with operators to compute the set of all sublists, and the set of objects stored in a list. Finally, we support constraints on sizes of sets, which gives us the ability to compute list length as well as the number of distinct list elements. We show that the extended theory is reducible to the theory of sets with linear cardinality constraints, and therefore still in NP. This reduction enables us to combine our theory with other decidable theories that impose constraints on sets of objects, which further increases the potential of our decidability result in verification of functional and imperative software.

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. Barrett, C., Shikanian, I., Tinelli, C.: An abstract decision procedure for satisfiability in the theory of recursive data types. ENTCS 174(8), 23–37 (2007)

    MATH  Google Scholar 

  2. Börger, E., Grädel, E., Gurevich, Y.: The Classical Decision Problem. Springer, Heidelberg (1997)

    Book  MATH  Google Scholar 

  3. Bouajjani, A., Dragoi, C., Enea, C., Sighireanu, M.: A Logic-Based Framework for Reasoning about Composite Data Structures. In: Bravetti, M., Zavattaro, G. (eds.) CONCUR 2009. LNCS, vol. 5710, pp. 178–195. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  4. Furia, C.A.: What’s Decidable about Sequences? In: Bouajjani, A., Chin, W.-N. (eds.) ATVA 2010. LNCS, vol. 6252, pp. 128–142. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  5. Ihlemann, C., Sofronie-Stokkermans, V.: System Description: H-PILoT. In: Schmidt, R.A. (ed.) CADE-22. LNCS, vol. 5663, pp. 131–139. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  6. Jacobs, S.: Incremental Instance Generation in Local Reasoning. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 368–382. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  7. Jaffar, J.: Minimal and complete word unification. J. ACM 37(1), 47–85 (1990)

    Article  MathSciNet  MATH  Google Scholar 

  8. Kuncak, V., Rinard, M.: Towards Efficient Satisfiability Checking for Boolean Algebra with Presburger Arithmetic. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 215–230. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  9. Lahiri, S., Qadeer, S.: Back to the future: revisiting precise program verification using SMT solvers. In: POPL (2008)

    Google Scholar 

  10. Lev-Ami, T., Immerman, N., Reps, T., Sagiv, M., Srivastava, S., Yorsh, G.: Simulating Reachability using First-Order Logic with Applications to Verification of Linked Data Structures. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol. 3632, pp. 99–115. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  11. Makanin, G.: The problem of solvability of equations in a free semigroup. Math. USSR Sbornik, 129–198 (1977); AMS (1979)

    Google Scholar 

  12. Nguyen, H.H., David, C., Qin, S., Chin, W.-N.: Automated Verification of Shape, Size and Bag Properties Via Separation Logic. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol. 4349, pp. 251–266. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

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

    MATH  Google Scholar 

  14. Odersky, M., Spoon, L., Venners, B.: Programming in Scala: a comprehensive step-by-step guide. Artima Press (2008)

    Google Scholar 

  15. Oppen, D.C.: Reasoning about recursively defined data structures. In: POPL, pp. 151–157 (1978)

    Google Scholar 

  16. Piskac, R., Suter, P., Kuncak, V.: On decision procedures for ordered collections. Technical Report LARA-REPORT-2010-001, EPFL (2010)

    Google Scholar 

  17. Plandowski, W.: Satisfiability of word equations with constants is in PSPACE. J. ACM 51(3) (2004)

    Google Scholar 

  18. Sofronie-Stokkermans, V.: Hierarchic Reasoning in Local Theory Extensions. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol. 3632, pp. 219–234. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  19. Sofronie-Stokkermans, V.: Locality Results for Certain Extensions of Theories with Bridging Functions. In: Schmidt, R.A. (ed.) CADE-22. LNCS, vol. 5663, pp. 67–83. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  20. Suter, P., Dotta, M., Kuncak, V.: Decision procedures for algebraic data types with abstractions. In: POPL (2010)

    Google Scholar 

  21. Venkataraman, K.N.: Decidability of the purely existential fragment of the theory of term algebras. Journal of the ACM (JACM) 34(2), 492–510 (1987)

    Article  MathSciNet  Google Scholar 

  22. Wies, T., Muñiz, M., Kuncak, V.: On deciding functional lists with sublist sets. Technical Report EPFL-REPORT-148361, EPFL (2010), http://cs.nyu.edu/~wies/publ/on_deciding_functional_lists_with_sublist_sets.pdf

  23. Wies, T., Muñiz, M., Kuncak, V.: An Efficient Decision Procedure for Imperative Tree Data Structures. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS, vol. 6803, pp. 476–491. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  24. Wies, T., Piskac, R., Kuncak, V.: Combining Theories with Shared Set Operations. In: Ghilardi, S., Sebastiani, R. (eds.) FroCoS 2009. LNCS, vol. 5749, pp. 263–278. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  25. Yessenov, K., Kuncak, V., Piskac, R.: Collections, Cardinalities, and Relations. In: Barthe, G., Hermenegildo, M. (eds.) VMCAI 2010. LNCS, vol. 5944, pp. 380–395. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  26. Zee, K., Kuncak, V., Rinard, M.: Full functional verification of linked data structures. In: PLDI (2008)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. New York University, New York, NY, USA

    Thomas Wies

  2. University of Freiburg, Germany

    Marco Muñiz

  3. EPFL, Switzerland

    Viktor Kuncak

Authors
  1. Thomas Wies
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Marco Muñiz
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Viktor Kuncak
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. MS 301-285, 4800 Oak Grove Drive, 91109, Pasadena, CA, USA

    Rajeev Joshi

  2. ETH Zürich, Universitätstr. 6, 8092, Zürich, Switzerland

    Peter Müller

  3. Department of Computer Science, University of Freiburg, Georges-Köhler-Allee 52, 79110, Freiburg, Germany

    Andreas Podelski

Rights and permissions

Reprints and permissions

Copyright information

© 2012 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Wies, T., Muñiz, M., Kuncak, V. (2012). Deciding Functional Lists with Sublist Sets. In: Joshi, R., Müller, P., Podelski, A. (eds) Verified Software: Theories, Tools, Experiments. VSTTE 2012. Lecture Notes in Computer Science, vol 7152. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-27705-4_6

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-27705-4_6

  • Publisher Name: Springer, Berlin, Heidelberg

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

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

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation