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


Published in:
Computer Science Logic, 6247, 34-48
Presented at:
Annual Conference of the European Association for Computer Science Logic, Brno, CZ, Aug 23-27, 2010
Year:
2010
Publisher:
Springer-Verlag New York, Ms Ingrid Cunningham, 175 Fifth Ave, New York, Ny 10010 Usa
ISBN:
978-3-642-15204-7
Keywords:
Laboratories:




 Record created 2012-01-10, last modified 2018-09-13


Rate this document:

Rate this document:
1
2
3
 
(Not yet reviewed)