Encoding TLA+ into unsorted and many-sorted first-order logic

Stephan Merz 1 Hernán Vanzetto 1, 2
1 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Abstract : TLA+ is a specification language designed for the verification of concurrent and distributed algorithms and systems. We present an encoding of a non-temporal fragment of TLA+ into (unsorted) first-order logic and many-sorted first-order logic, the input languages of first-order automated theorem provers. The non-temporal subset of TLA+ is based on untyped set theory and includes functions, arithmetic expressions, and Hilbert's choice operator. The translation, based on encoding techniques such as boolification, injection of unsorted expressions into sorted languages, term rewriting, and abstraction, is the core component of a back-end prover based on first-order theorem provers and SMT solvers for the TLA+ Proof System.
Type de document :
Article dans une revue
Science of Computer Programming, Elsevier, 2018, 158, pp.3-20. 〈10.1016/j.scico.2017.09.004〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01768750
Contributeur : Stephan Merz <>
Soumis le : mardi 17 avril 2018 - 14:11:28
Dernière modification le : mercredi 18 avril 2018 - 09:20:34

Fichier

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

Identifiants

Collections

Citation

Stephan Merz, Hernán Vanzetto. Encoding TLA+ into unsorted and many-sorted first-order logic. Science of Computer Programming, Elsevier, 2018, 158, pp.3-20. 〈10.1016/j.scico.2017.09.004〉. 〈hal-01768750〉

Partager

Métriques

Consultations de la notice

103

Téléchargements de fichiers

33