TLA + is a formal specification language that is based on ZF set theory and the Temporal Logic of Actions TLA. The TLA + proof system tlaps assists users in deductively verifying safety properties of TLA + specifications. tlaps is built around a proof manager, which interprets the TLA + proof language, generates corresponding proof obligations, and passes them to backend verifiers. In this paper we present a new backend for use with SMT solvers that supports elementary set theory, functions, arithmetic, tuples, and records. Type information required by the solvers is provided by a typing discipline for TLA + proof obligations, which helps us disambiguate the translation of expressions of (untyped) TLA + , while ensuring its soundness. Preliminary results show that the backend can help to significantly increase the degree of automation of certain interactive proofs. © 2012 Springer-Verlag.
CITATION STYLE
Merz, S., & Vanzetto, H. (2012). Automatic Verification of TLA + proof obligations with SMT solvers. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7180 LNCS, pp. 289–303). https://doi.org/10.1007/978-3-642-28717-6_23
Mendeley helps you to discover research relevant for your work.