Publication
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.
Volkan Cevher, Grigorios Chrysos, Efstratios Panteleimon Skoulakis
Viktor Kuncak, Simon Guilloud, Sankalp Gambhir