Ordered Sets in the Calculus of Data Structures (Invited Paper)

paper ps   
Our goal is to identify families of relations that are useful for reasoning about software. We describe such families using decidable quantifier-free classes of logical constraints with a rich set of operations. A key challenge is to define such classes of constraints in a modular way, by combining multiple decidable classes. Working with quantifier-free combinations of constraints makes the combination agenda more realistic and the resulting logics more likely to be tractable than in the presence of quantifiers. Our approach to combination is based on reducing decidable fragments to a common class, Boolean Algebra with Presburger Arithmetic (BAPA). This logic was introduced by Feferman and Vaught in 1959 and can express properties of uninterpreted sets of elements, with set algebra operations and equicardinality relation (consequently, it can also express Presburger arithmetic constraints on cardinalities of sets). Combination by reduction to BAPA allows us to obtain decidable quantifier-free combinations of decidable logics that share BAPA operations. We use the term Calculus of Data Structures to denote a family of decidable constraints that reduce to BAPA. This class includes, for example, combinations of formulas in BAPA, weak monadic second-order logic of k-successors, two-variable logic with counting, and term algebras with certain homomorphisms. The approach of reduction to BAPA generalizes the Nelson-Oppen combination that forms the foundation of constraint solvers used in software verification. BAPA is convenient as a target for reductions because it admits quantifier elimination and its quantifier-free fragment is NP-complete. We describe a new member of the Calculus of Data Structures: a quantifier-free fragment that supports 1) boolean algebra of finite and infinite sets of real numbers, 2) linear arithmetic over real numbers, 3) formulas that can restrict chosen set or element variables to range over integers (providing, among others, the power of mixed integer arithmetic and sets of integers), 4) the cardinality operators, stating whether a given set has a given finite cardinality or is infinite, 5) infimum and supremum operators on sets. Among the applications of this logic are reasoning about the externally observable behavior of data structures such as sorted lists and priority queues, and specifying witness functions for the BAPA synthesis problem. We describe an abstract reduction to BAPA for our logic, proving that the satisfiability of the logic is in NP and that it can be combined with the other fragments of the Calculus of Data Structures.

Citation

Viktor Kuncak, Ruzica Piskac, and Philippe Suter. Ordered sets in the calculus of data structures (invited paper). In CSL, 2010.

BibTex Entry

@inproceedings{KuncakETAL10OrderedSetsinCalculusofDataStructures,
  author = {Viktor Kuncak and Ruzica Piskac and Philippe Suter},
  title = {Ordered Sets in the Calculus of Data Structures (Invited Paper)},
  booktitle = {CSL},
  abstract = {Our goal is to identify families of relations that are
useful for reasoning about software. We describe such
families using decidable quantifier-free classes of logical
constraints with a rich set of operations.  A key challenge
is to define such classes of constraints in a modular way,
by combining multiple decidable classes. Working with
quantifier-free combinations of constraints makes the
combination agenda more realistic and the resulting logics
more likely to be tractable than in the presence of
quantifiers.
Our approach to combination is based on reducing decidable
fragments to a common class, Boolean Algebra with Presburger
Arithmetic (BAPA). This logic was introduced by
Feferman and Vaught in 1959 and can express properties of
uninterpreted sets of elements, with set algebra operations
and equicardinality relation (consequently, it can also
express Presburger arithmetic constraints on cardinalities
of sets).  Combination by reduction to BAPA allows us to
obtain decidable quantifier-free combinations of decidable
logics that share BAPA operations.  We use the
term Calculus of Data Structures to denote a family
of decidable constraints that reduce to BAPA. This class
includes, for example, combinations of formulas in BAPA,
weak monadic second-order logic of k-successors,
two-variable logic with counting, and term algebras with
certain homomorphisms.  The approach of reduction to BAPA
generalizes the Nelson-Oppen combination that forms the
foundation of constraint solvers used in software
verification.  BAPA is convenient as a target for reductions
because it admits quantifier elimination and its
quantifier-free fragment is NP-complete.
We describe a new member of the Calculus of Data Structures:
a quantifier-free fragment that supports 1) boolean algebra
of finite and infinite sets of real numbers, 2) linear
arithmetic over real numbers, 3) formulas that can restrict
chosen set or element variables to range over integers
(providing, among others, the power of mixed integer
arithmetic and sets of integers), 4) the cardinality
operators, stating whether a given set has a given finite
cardinality or is infinite, 5) infimum and supremum
operators on sets.  Among the applications of this logic are
reasoning about the externally observable behavior of data
structures such as sorted lists and priority queues, and
specifying witness functions for the BAPA synthesis problem.
We describe an abstract reduction to BAPA for our logic,
proving that the satisfiability of the logic is in NP and
that it can be combined with the other fragments of the
Calculus of Data Structures.
},
  year = 2010
}