AlloyPE: An SMT-based Proof Engine for Alloy
AlloyPE is a proof engine for system specifications written in Alloy - a declarative first-order relational logic with built-in operators for transitive closure and cardinality. AlloyPE is fully automatic; when it outputs "unsat", the property has been soundly proven, and when it outputs "sat", a sound counterexample has been found. However, it may also time-out or output "unknown" due to the undecidability of the logic. The engine works via a sound translation from the Alloy language to SMT-LIB - the input language of several Satisfiability Modulo Theories (SMT) solvers. The translation is tailored to exploit the increasing capability of modern SMT solvers in handling first-order quantifiers in the unbounded context. In our experiments, we could prove a considerable number of non-trivial system specifications written in Alloy, see the publications below.
- A Dual-Engine for Early Analysis of Critical Systems, Aboubakr Achraf El Ghazi, Ulrich Geilmann, Mattias Ulbrich, Mana Taghdiri, Workshop on Dependable Software for Critical Infrastructures (DSCI), 2011.
- Relational Reasoning via SMT Solving, Aboubakr Achraf El Ghazi, Mana Taghdiri, International Symposium on Formal Methods (FM), 2011.
- Analyzing Alloy Formulas using an SMT Solver: A Case Study, Aboubakr Achraf El Ghazi, Mana Taghdiri. International Workshop on Automated Formal Methods (AFM), 2010.