Automatic Verification Of TLA+ Proof Obligations With SMT Solvers

Abstract : TLA+ is a formal specification language that is based on ZF set theory and the Temporal Logic of Actions TLA. The TLA+ proof system TLAPS assists users in deductively verifying safety properties of TLA+ specifications. TLAPS is built around a proof manager, which interprets the TLA+ proof language, generates corresponding proof obligations, and passes them to backend verifiers. In this paper we present a new backend for use with SMT solvers that supports elementary set theory, functions, arithmetic, tuples, and records. Type information required by the solvers is provided by a typing discipline for TLA+ proof obligations, which helps us disambiguate the translation of expressions of (untyped) TLA+, while ensuring its soundness. Preliminary results show that the backend can help to significantly increase the degree of automation of certain interactive proofs.
Type de document :
Communication dans un congrès
Nikolaj Bjørner and Andrei Voronkov. 18th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR-18), Mar 2012, Mérida, Venezuela. Springer, 7180, pp.289-303, 2012, Lecture Notes in Computer Science. 〈10.1007/978-3-642-28717-6_23〉
Liste complète des métadonnées

Littérature citée [12 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00760570
Contributeur : Stephan Merz <>
Soumis le : mardi 4 décembre 2012 - 09:51:59
Dernière modification le : jeudi 11 janvier 2018 - 06:23:13
Document(s) archivé(s) le : samedi 17 décembre 2016 - 19:30:19

Fichiers

tla2smt.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Stephan Merz, Hernán Vanzetto. Automatic Verification Of TLA+ Proof Obligations With SMT Solvers. Nikolaj Bjørner and Andrei Voronkov. 18th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR-18), Mar 2012, Mérida, Venezuela. Springer, 7180, pp.289-303, 2012, Lecture Notes in Computer Science. 〈10.1007/978-3-642-28717-6_23〉. 〈hal-00760570〉

Partager

Métriques

Consultations de la notice

254

Téléchargements de fichiers

264