zbMATH — the first resource for mathematics

A proof assistant for Alloy specifications. (English) Zbl 1352.68166
Flanagan, Cormac (ed.) et al., Tools and algorithms for the construction and analysis of systems. 18th international conference, TACAS 2012, held as part of the European joint conferences on theory and practice of software, ETAPS 2012, Tallinn, Estonia, March 24 – April 1, 2012. Proceedings. Berlin: Springer (ISBN 978-3-642-28755-8/pbk). Lecture Notes in Computer Science 7214, 422-436 (2012).
Summary: Alloy is a specification language based on a relational first-order logic with built-in operators for transitive closure, set cardinality, and integer arithmetic. The Alloy Analyzer checks Alloy specifications automatically with respect to bounded domains. Thus, while suitable for finding counterexamples, it cannot, in general, provide correctness proofs. This paper presents Kelloy, a tool for verifying Alloy specifications with respect to potentially infinite domains. It describes an automatic translation of the full Alloy language to the first-order logic of the KeY theorem prover, and an Alloy-specific extension to KeY’s calculus. It discusses correctness and completeness conditions of the translation, and reports on our automatic and interactive experiments.
For the entire collection see [Zbl 1238.68014].
68Q60 Specification and verification (program logics, model checking, etc.)
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
Alloy; Athena; JKelloy; Kelloy; KeY; PVS
Full Text: DOI