Aboubakr Achraf El Ghazi, Mana Taghdiri

17th International Symposium on Formal Methods (FM), 2011.

Abstract:

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.