Automated Software Analysis Group


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.



Tool and Experiments

The Kelloy tool and some experiments can be downloaded from here: