Kelloy

Kelloy is an interactive proof system for specifications written in Alloy - a declarative first-order relational logic with built-in operators for transitive closure and cardinality.

Kelloy uses KeY as a proving backend. Alloy specifications are automatically translated to proof obligations in KeY's first-order logic. The interactive proof process is supported by an automation strategy specifically tailored for Alloy specifications.

Kelloy is complete (modulo integers). However, since proving specifications with Kelloy potentially requires user-interaction, we suggest using automated tools like AlloyPE first, and give only those problems to Kelloy for which automation could not be achieved.

Publications

• A Proof Assistant for Alloy Specifications, Mattias Ulbrich, Ulrich Geilmann, Aboubakr Achraf El Ghazi, Mana Taghdiri, In 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2012.
• On Proving Alloy Specifications using KeY, Mattias Ulbrich, Ulrich Geilmann, Aboubakr Achraf El Ghazi, Mana Taghdiri, Karlsruhe Institute of Technology, Technical report 2011-37, 2011.
• Verifying Alloy Models Using KeY, Ulrich Geilmann, Karlsruhe Institute of Technology, Diplomarbeit, 2011.
• 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.

People

• Ulrich Geilmann
• Mana Taghdiri
• Aboubakr Achraf El Ghazi
• Mattias Ulbirch

Tool and Experiments

The Kelloy tool and some experiments can be downloaded from here: http://i12www.ira.uka.de/~elghazi/kelloyExp