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
Volume5944 LNCS
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)03029743
ISSN (Electronic)16113349

Other

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

Fingerprint

Data structures
Data Structures
Calculus
Logic
Multiset
Algebra
Boolean algebra
Computability and decidability
Many to one
Monadic Second-order Logic
Software Verification
Heap
Decision Procedures
Acoustic waves
First-order Logic
Decidability
Type Systems
Specifications
Predicate
Counting

ASJC Scopus subject areas

  • Computer Science(all)
  • Theoretical Computer Science

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 (Vol. 5944 LNCS, 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

Building a calculus of data structures. / Kuncak, Viktor; Piskac, Ruzica; Suter, Philippe; Wies, Thomas.

Verification, Model Checking, and Abstract Interpretation - 11th International Conference, VMCAI 2010, Proceedings. Vol. 5944 LNCS 2010. p. 26-44 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 5944 LNCS).

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

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. vol. 5944 LNCS, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 5944 LNCS, pp. 26-44, 11th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2010, Madrid, Spain, 1/17/10. https://doi.org/10.1007/978-3-642-11319-2_6
Kuncak V, Piskac R, Suter P, Wies T. Building a calculus of data structures. In Verification, Model Checking, and Abstract Interpretation - 11th International Conference, VMCAI 2010, Proceedings. Vol. 5944 LNCS. 2010. p. 26-44. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-642-11319-2_6
Kuncak, Viktor ; Piskac, Ruzica ; Suter, Philippe ; Wies, Thomas. / Building a calculus of data structures. Verification, Model Checking, and Abstract Interpretation - 11th International Conference, VMCAI 2010, Proceedings. Vol. 5944 LNCS 2010. pp. 26-44 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{3ff8bf595fe646818cbc92a13f0bfdf5,
title = "Building a calculus of data structures",
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{\"o}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.",
author = "Viktor Kuncak and Ruzica Piskac and Philippe Suter and Thomas Wies",
year = "2010",
doi = "10.1007/978-3-642-11319-2_6",
language = "English (US)",
isbn = "3642113184",
volume = "5944 LNCS",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
pages = "26--44",
booktitle = "Verification, Model Checking, and Abstract Interpretation - 11th International Conference, VMCAI 2010, Proceedings",

}

TY - GEN

T1 - Building a calculus of data structures

AU - Kuncak, Viktor

AU - Piskac, Ruzica

AU - Suter, Philippe

AU - Wies, Thomas

PY - 2010

Y1 - 2010

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=77949443933&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=77949443933&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-11319-2_6

DO - 10.1007/978-3-642-11319-2_6

M3 - Conference contribution

AN - SCOPUS:77949443933

SN - 3642113184

SN - 9783642113185

VL - 5944 LNCS

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 26

EP - 44

BT - Verification, Model Checking, and Abstract Interpretation - 11th International Conference, VMCAI 2010, Proceedings

ER -