A Proof Assistant for Alloy Specifications

Reviewed Paper In Proceedings

Author(s):Mattias Ulbrich, Ulrich Geilmann, Aboubakr Achraf El Ghazi, and Mana Taghdiri
In:18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2012)
Publisher:Springer
Series:LNCS
Volume:7214
Year:2012
Pages:422-436
DOI:10.1007/978-3-642-28756-5_29
Links:

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.

BibTeX

@INPROCEEDINGS{ulbrich-geilmann-elghazi-taghdiri-tacas2012,
  author = {Mattias Ulbrich and Ulrich Geilmann and Aboubakr Achraf {El Ghazi}
	and Mana Taghdiri},
  title = {A Proof Assistant for {Alloy} Specifications},
  booktitle = {18th International Conference on Tools and Algorithms for the Construction
	and Analysis of Systems (TACAS 2012)},
  year = {2012},
  volume = {7214},
  series = {LNCS},
  pages = {422--436},
  month = {March},
  publisher = {Springer},
  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.},
  doi = {10.1007/978-3-642-28756-5_29},
  links = {PDF:http://lfm.iti.uni-karlsruhe.de/files/publications/ProofAssistantForAlloySpecifications.pdf;
	Slides:http://lfm.iti.uni-karlsruhe.de/files/publications/elghazi_tacas2012.final.pdf;
	Technical Report:http://digbib.ubka.uni-karlsruhe.de/volltexte/1000025523}
}