Building a calculus of data structures

Viktor Kuncak, Ruzica Piskac, Philippe Suter, Thomas Wies

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

Techniques such as verification condition generation, predicate abstraction, and expressive type systems reduce software verification to proving formulas in expressive logics. Programs and their specifications often make use of data structures such as sets, multisets, algebraic data types, or graphs. Consequently, formulas generated from verification also involve such data structures. To automate the proofs of such formulas we propose a logic (a "calculus") of such data structures. We build the calculus by starting from decidable logics of individual data structures, and connecting them through functions and sets, in ways that go beyond the frameworks such as Nelson-Oppen. The result are new decidable logics that can simultaneously specify properties of different kinds of data structures and overcome the limitations of the individual logics. Several of our decidable logics include abstraction functions that map a data structure into its more abstract view (a tree into a multiset, a multiset into a set), into a numerical quantity (the size or the height), or into the truth value of a candidate data structure invariant (sortedness, or the heap property). For algebraic data types, we identify an asymptotic many-to-one condition on the abstraction function that guarantees the existence of a decision procedure. In addition to the combination based on abstraction functions, we can combine multiple data structure theories if they all reduce to the same data structure logic. As an instance of this approach, we describe a decidable logic whose formulas are propositional combinations of formulas in: weak monadic second-order logic of two successors, two-variable logic with counting, multiset algebra with Presburger arithmetic, the Bernays-Schönfinkel-Ramsey class of first-order logic, and the logic of algebraic data types with the set content function. The subformulas in this combination can share common variables that refer to sets of objects along with the common set algebra operations. Such sound and complete combination is possible because the relations on sets definable in the component logics are all expressible in Boolean Algebra with Presburger Arithmetic. Presburger arithmetic and its new extensions play an important role in our decidability results. In several cases, when we combine logics that belong to NP, we can prove the satisfiability for the combined logic is still in NP.

Original languageEnglish (US)
Title of host publicationVerification, Model Checking, and Abstract Interpretation - 11th International Conference, VMCAI 2010, Proceedings
Pages26-44
Number of pages19
DOIs
StatePublished - 2010
Event11th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2010 - Madrid, Spain
Duration: Jan 17 2010Jan 19 2010

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume5944 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other11th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2010
CountrySpain
CityMadrid
Period1/17/101/19/10

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Building a calculus of data structures'. Together they form a unique fingerprint.

  • Cite this

    Kuncak, V., Piskac, R., Suter, P., & Wies, T. (2010). Building a calculus of data structures. In Verification, Model Checking, and Abstract Interpretation - 11th International Conference, VMCAI 2010, Proceedings (pp. 26-44). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 5944 LNCS). https://doi.org/10.1007/978-3-642-11319-2_6