A Proof Assistant for Alloy Specifications
| العنوان: | A Proof Assistant for Alloy Specifications |
|---|---|
| المؤلفون: | Ulrich Geilmann, Mattias Ulbrich, Mana Taghdiri, Aboubakr Achraf El Ghazi |
| المصدر: | Tools and Algorithms for the Construction and Analysis of Systems ISBN: 9783642287558 TACAS |
| بيانات النشر: | Springer Berlin Heidelberg, 2012. |
| سنة النشر: | 2012 |
| مصطلحات موضوعية: | Correctness, Theoretical computer science, Programming language, Proof assistant, Transitive closure, Sequent calculus, Specification language, computer.software_genre, Condensed Matter::Materials Science, Automated theorem proving, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, Alloy Analyzer, Software_SOFTWAREENGINEERING, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, Completeness (logic), computer, Mathematics |
| الوصف: | 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. |
| ردمك: | 978-3-642-28755-8 |
| DOI: | 10.1007/978-3-642-28756-5_29 |
| URL الوصول: | https://explore.openaire.eu/search/publication?articleId=doi_________::433c4f4293fdab2654518e0e40023da3 https://doi.org/10.1007/978-3-642-28756-5_29 |
| Rights: | OPEN |
| رقم الانضمام: | edsair.doi...........433c4f4293fdab2654518e0e40023da3 |
| قاعدة البيانات: | OpenAIRE |
| ردمك: | 9783642287558 |
|---|---|
| DOI: | 10.1007/978-3-642-28756-5_29 |