Automated Software Analysis Group

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.






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.