Encoding TLA+ into Many-Sorted First-Order Logic

Abstract : This paper presents an encoding of a non-temporal fragment of the TLA+ language, which includes untyped set theory, functions, arithmetic expressions, and Hilbert's ε operator, into many-sorted first-order logic, the input language of state-of-the-art SMT solvers. This 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 SMT solvers for the TLA+ Proof System.
Type de document :
Communication dans un congrès
Michael J. Butler; Klaus-Dieter Schewe; Atif Mashkoor; Miklós Biró. Abstract State Machines, Alloy, B, TLA, VDM, and Z - 5th International Conference, ABZ 2016, 2016, Linz, Austria. Springer, 9675, pp.54-69, 2016, 〈10.1007/978-3-319-33600-8_3〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01322328
Contributeur : Stephan Merz <>
Soumis le : vendredi 27 mai 2016 - 09:15:51
Dernière modification le : mercredi 8 novembre 2017 - 12:08:09

Fichier

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

Identifiants

Collections

Citation

Stephan Merz, Hernán Vanzetto. Encoding TLA+ into Many-Sorted First-Order Logic. Michael J. Butler; Klaus-Dieter Schewe; Atif Mashkoor; Miklós Biró. Abstract State Machines, Alloy, B, TLA, VDM, and Z - 5th International Conference, ABZ 2016, 2016, Linz, Austria. Springer, 9675, pp.54-69, 2016, 〈10.1007/978-3-319-33600-8_3〉. 〈hal-01322328〉

Partager

Métriques

Consultations de
la notice

177

Téléchargements du document

89