This paper explores the idea of using a SAT Modulo Theories (SMT) solver for proving properties of relational specifications. The goal is to automatically establish or refute consistency of a set of constraints expressed in a first-order relational logic, namely Alloy, without limiting the analysis to a bounded scope. Existing analysis of relational constraints - as performed by the Alloy Analyzer - is based on SAT solving and thus requires finitizing the set of values that each relation can take. Our technique complements this approach by axiomatizing all relational operators in a first-order SMT logic, and taking advantage of the background theories supported by SMT solvers. Consequently, it can potentially prove that a formula is a tautology - a capability completely missing from the Alloy Analyzer - and generate a counterexample when the proof fails. We also report on our experiments of applying this technique to various systems specified in Alloy. © 2011 Springer-Verlag.
CITATION STYLE
El Ghazi, A. A., & Taghdiri, M. (2011). Relational reasoning via SMT solving. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6664 LNCS, pp. 133–148). https://doi.org/10.1007/978-3-642-21437-0_12
Mendeley helps you to discover research relevant for your work.