Home | Legals | Data Protection | Sitemap | KIT

Relational Reasoning via SMT Solving

Relational Reasoning via SMT Solving

Aboubakr Achraf El Ghazi, Mana Taghdiri


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


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.


    author    = {Aboubakr Achraf {El Ghazi} and Mana Taghdiri},
    title     = {Relational Reasoning via {SMT} Solving},
    booktitle = {17th International Symposium on Formal Methods (FM)},
    pages     = {133-148},
    year      = {2011},
    month     = {June}