Sciweavers

CSL
2010
Springer

Ordered Sets in the Calculus of Data Structures

13 years 11 months ago
Ordered Sets in the Calculus of Data Structures
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 quantifierfree 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 quantifi...
Viktor Kuncak, Ruzica Piskac, Philippe Suter
Added 08 Nov 2010
Updated 08 Nov 2010
Type Conference
Year 2010
Where CSL
Authors Viktor Kuncak, Ruzica Piskac, Philippe Suter
Comments (0)