Home | Legals | Sitemap | KIT

Proving Alloy models by introducing an explicit relational theory in SMT

Proving Alloy models by introducing an explicit relational theory in SMT
Author:

Jonathan Best

links:
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.

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.}
}