2012/09/25 by Nuno Macedo, Alcino Cunha, Macedo, Nuno +1 · 1 citation
Computer Science · #FOS: Computer and information sciences #Formal Languages and Automata Theory (cs.FL) #Formal Methods in Verification #Logic, programming, and type systems #Security and Verification in Computing #cs.FL
paper · pdf · doi:10.48550/arxiv.1209.5773
arxiv created 2012/09/25 · openalex publication_date 2012/09/25 · arxiv updated 2012/09/27 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
Alloy is an increasingly popular lightweight specification language based on relational logic. Alloy models can be automatically verified within a bounded scope using off-the-shelf SAT solvers. Since false assertions can usually be disproved using small counter-examples, this approach suffices for most applications. Unfortunately, it can sometimes lead to a false sense of security, and in critical applications a more traditional unbounded proof may be required. The automatic theorem prover Prover9 has been shown to be particularly effective for proving theorems of relation algebras [7], a quantifier-free (or point-free) axiomatization of a fragment of relational logic. In this paper we propose a translation from Alloy specifications to fork algebras (an extension of relation algebras with the same expressive power as relational logic) which enables their unbounded verification in Prover9. This translation covers not only logic assertions, but also the structural aspects (namely type declarations), and was successfully implemented and applied to several examples.