Book chapter
Relational Constraint Solving in SMT
Automated Deduction – CADE 26, pp.148-165
Lecture Notes in Computer Science, Springer International Publishing
07/11/2017
DOI: 10.1007/978-3-319-63046-5_10
Abstract
Relational logic is useful for reasoning about computational problems with relational structures, including high-level system design, architectural configurations of network systems, ontologies, and verification of programs with linked data structures. We present a modular extension of an earlier calculus for the theory of finite sets to a theory of finite relations with such operations as transpose, product, join, and transitive closure. We implement this extension as a theory solver of the SMT solver CVC4. Combining this new solver with the finite model finding features of CVC4 enables several compelling use cases. For instance, native support for relations enables a natural mapping from Alloy, a declarative modeling language based on first-order relational logic, to SMT constraints. It also enables a natural encoding of several description logics with concrete domains, allowing the use of an SMT solver to analyze, for instance, Web Ontology Language (OWL) models. We provide an initial evaluation of our solver on a number of Alloy and OWL models which shows promising results.
Details
- Title: Subtitle
- Relational Constraint Solving in SMT
- Creators
- Baoluo Meng - Department of Computer Science, The University of Iowa, Iowa City, USAAndrew Reynolds - Department of Computer Science, The University of Iowa, Iowa City, USACesare Tinelli - Department of Computer Science, The University of Iowa, Iowa City, USAClark Barrett - Department of Computer Science, Stanford University, Stanford, USA
- Resource Type
- Book chapter
- Publication Details
- Automated Deduction – CADE 26, pp.148-165
- Publisher
- Springer International Publishing; Cham
- Series
- Lecture Notes in Computer Science
- DOI
- 10.1007/978-3-319-63046-5_10
- eISSN
- 1611-3349
- ISSN
- 0302-9743
- Language
- English
- Date published
- 07/11/2017
- Academic Unit
- Computer Science
- Record Identifier
- 9984002458802771
Metrics
24 Record Views