Proving Alloy models by introducing an explicit relational theory in SMT

Author:
Jonathan Best
Place:
Karlsruhe Institute of Technology, Studienarbeit, 2012
Date: Dec. 2012
Abstract:

This thesis demonstrates that Alloy problems can be proven by using solvers for Satisfiability Modulo Theories (SMT) while preserving the structure of the original problem. The verification condition of the Alloy problem is translated from Alloy to an equi-satisfiable problem in the language of SMT-LIB. The translation is extended with lemmas and shown to be efficiently provable. Furthermore, we motivate a systematic way for finding these lemmas using a hand-written proof and evaluate the process in a case report. The proof is also included in this work.

links

[pdf]

BibTex

@studyThesis{best-sa-2012,
    author = "Jonathan Best",
    title  = {Proving Alloy models by introducing an explicit relational theory in SMT},
    school = {Karlsruhe Institute of Technology},
    type   = {Studienarbeit},
    year   = {2012},
    month  = {Dec.}
}