Encoding TLA+ into unsorted and many-sorted first-order logic - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Article Dans Une Revue Science of Computer Programming Année : 2018

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

Résumé

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.
Fichier principal
Vignette du fichier
tla2smt2_v3.pdf (396.46 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-01768750 , version 1 (17-04-2018)

Identifiants

Citer

Stephan Merz, Hernán Vanzetto. Encoding TLA+ into unsorted and many-sorted first-order logic. Science of Computer Programming, 2018, 158, pp.3-20. ⟨10.1016/j.scico.2017.09.004⟩. ⟨hal-01768750⟩
135 Consultations
286 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More