Encoding TLA+ into Many-Sorted First-Order Logic - Archive ouverte HAL Access content directly
Conference Papers Year : 2016

Encoding TLA+ into Many-Sorted First-Order Logic

(1, 2, 3) , (4)
1
2
3
4

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.
Fichier principal
Vignette du fichier
tla2smt.pdf (316.86 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

hal-01322328 , version 1 (27-05-2016)

Identifiers

Cite

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⟩
255 View
358 Download

Altmetric

Share

Gmail Facebook Twitter LinkedIn More