Encoding TLA+ into Many-Sorted First-Order Logic

Stephan Merz 1, 2, 3 Hernán Vanzetto 4
1 MOSEL - Proof-oriented development of computer-based systems
LORIA - FM - Department of Formal Methods
2 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
MPII - Max-Planck-Institut für Informatik, Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
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.
Document type :
Conference papers
Complete list of metadatas

Cited literature [16 references]  Display  Hide  Download

https://hal.inria.fr/hal-01322328
Contributor : Stephan Merz <>
Submitted on : Friday, May 27, 2016 - 9:15:51 AM
Last modification on : Tuesday, February 19, 2019 - 3:40:03 PM

File

tla2smt.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Stephan Merz, Hernán Vanzetto. Encoding TLA+ into Many-Sorted First-Order Logic. Abstract State Machines, Alloy, B, TLA, VDM, and Z - 5th International Conference, ABZ 2016, 2016, Linz, Austria. pp.54-69, ⟨10.1007/978-3-319-33600-8_3⟩. ⟨hal-01322328⟩

Share

Metrics

Record views

329

Files downloads

287