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.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Abrial, J.-R., Hallerstede, S.: Refinement, decomposition, and instantiation of discrete models: Application to Event-B. Fundamenta Informaticae (2007)
Arkoudas, K., Khurshid, S., Marinov, D., Rinard, M.: Integrating model checking and theorem proving for relational reasoning. In: RMICS (2003)
Beckert, B., Hähnle, R., Schmitt, P.H. (eds.): Verification of Object-Oriented Software. LNCS (LNAI), vol. 4334. Springer, Heidelberg (2007)
Buss, S.R.: First-order proof theory of arithmetic. In: Handbook of Proof Theory, pp. 79–147. Elsevier (1998)
van Eijck, J.: Defining (reflexive) transitive closure on finite models, http://homepages.cwi.nl/~jve/papers/08/pdfs/FinTransClosRev.pdf
El Ghazi, A.A., Geilmann, U., Ulbrich, M., Taghdiri, M.: A Dual-Engine for Early Analysis of Critical Systems. In: DSCI (2011)
El Ghazi, A.A., Taghdiri, M.: Analyzing Alloy Constraints using an SMT Solver: A Case Study. In: AFM (2010)
El Ghazi, A.A., Taghdiri, M.: Relational Reasoning via SMT Solving. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol. 6664, pp. 133–148. Springer, Heidelberg (2011)
Fortune, S., Leivant, D., O’Donnell, M.: The expressiveness of simple and second-order type structures. J. ACM (1983)
Frias, M., Pombo, C.G.L.: Interpretability of first-order linear temporal logics in fork algebras. In: Journal of logic and algebraic programming (2006)
Frias, M.F., Pombo, C.G.L., Aguirre, N.M.: An Equational Calculus for Alloy. In: Davies, J., Schulte, W., Barnett, M. (eds.) ICFEM 2004. LNCS, vol. 3308, pp. 162–175. Springer, Heidelberg (2004)
Frias, M., Pombo, C.G.L., Baum, G., Aguirre, N.M., Maibaum, T.: Taking Alloy to the movies. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 678–697. Springer, Heidelberg (2003)
Frias, M.F., Pombo, C.G.L., Moscato, M.M.: Alloy Analyzer+PVS in the Analysis and Verification of Alloy Specifications. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 587–601. Springer, Heidelberg (2007)
Gentzen, G.: Untersuchungen über das logische Schließen. Mathematische Zeitschrift (1935)
Jackson, D.: Software Abstractions: Logic, Language and Analysis. MIT Press (2006)
Jackson, D., Wing, J.: Lightweight formal methods. IEEE Computer (1996)
Köker, C.: Discharging Event-B proof obligations. Studienarbeit, Universität Karlsruhe, TH (2008)
Lev-Ami, T., Immerman, N., Reps, T.W., Sagiv, M., Srivastava, S., Yorsh, G.: Simulating reachability using first-order logic with applications to verification of linked data structures. Logical Methods in Computer Science 5(2) (2009)
Shankar, N., Owre, S., Rushby, J., Stringer-Calvert, D.: PVS Prover Guide. Computer Science Laboratory, SRI International (1999)
Ulbrich, M., Geilmann, U., Ghazi, A.A.E., Taghdiri, M.: On proving alloy specifications using KeY. Tech. Rep. 2011-37, Karlsruhe Institute of Technology (2011)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ulbrich, M., Geilmann, U., El Ghazi, A.A., Taghdiri, M. (2012). A Proof Assistant for Alloy Specifications. In: Flanagan, C., König, B. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2012. Lecture Notes in Computer Science, vol 7214. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-28756-5_29
Download citation
DOI: https://doi.org/10.1007/978-3-642-28756-5_29
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-28755-8
Online ISBN: 978-3-642-28756-5
eBook Packages: Computer ScienceComputer Science (R0)