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.

Publications

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

People

• Mana Taghdiri
• Aboubakr Achraf El Ghazi
• Fikri Kabaksha
• Mihai Herda

Tool

We will be happy to share the tool upon your request. Please feel free to send an email to Achraf El Ghazi or Mana Taghdiri.