Abstract
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. © 2012 Springer-Verlag Berlin Heidelberg.
Cite
CITATION STYLE
Ulbrich, M., Geilmann, U., El Ghazi, A. A., & Taghdiri, M. (2012). A proof assistant for alloy specifications. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7214 LNCS, pp. 422–436). Springer Verlag. https://doi.org/10.1007/978-3-642-28756-5_29
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
