Towards certification of TLA+ proof obligations with SMT solvers

Stephan Merz 1, 2, 3 Hernán Vanzetto 1, 2, 3
1 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
2 MOSEL - Proof-oriented development of computer-based systems
LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : TLA+ is a formal specification language that is based on Zermelo-Fränkel 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. We introduce a typing discipline for TLA+ proof obligations, which helps us to disambiguate the translation of expressions of (untyped) TLA+, while ensuring its soundness. Our work is a first step towards the certification of proofs generated by proof-producing SMT solvers in Isabelle/TLA+, which is intended to be the only trusted component of TLAPS.
Type de document :
Communication dans un congrès
Pascal Fontaine and Aaron Stump. First International Workshop on Proof eXchange for Theorem Proving - PxTP 2011, Aug 2011, Wroclaw, Poland. 2011, 〈http://pxtp2011.loria.fr〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-00645458
Contributeur : Stephan Merz <>
Soumis le : lundi 28 novembre 2011 - 10:27:56
Dernière modification le : jeudi 11 janvier 2018 - 06:23:25
Document(s) archivé(s) le : lundi 5 décembre 2016 - 08:26:58

Fichier

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

Identifiants

  • HAL Id : hal-00645458, version 1

Collections

Citation

Stephan Merz, Hernán Vanzetto. Towards certification of TLA+ proof obligations with SMT solvers. Pascal Fontaine and Aaron Stump. First International Workshop on Proof eXchange for Theorem Proving - PxTP 2011, Aug 2011, Wroclaw, Poland. 2011, 〈http://pxtp2011.loria.fr〉. 〈hal-00645458〉

Partager

Métriques

Consultations de la notice

373

Téléchargements de fichiers

250