Automated Software Analysis Group

Relational Reasoning via SMT Solving

  • Author:

    Aboubakr Achraf El Ghazi, Mana Taghdiri

  • Place:

    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.


    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}