Automatic Verification Of TLA+ Proof Obligations With SMT Solvers

Stephan Merz and Hernán Vanzetto

Abstract

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.

© Springer-Verlag 2012

Available as: PDF

Reference

@InProceedings{merz:tlaplus-smt,
  author =       {Stephan Merz and Hern{\'{a}}n Vanzetto},
  title =        {Automatic Verification Of TLA\textsuperscript{+} Proof Obligations With SMT Solvers},
  booktitle = {18th Intl. Conf. Logic for Programming, Artificial Intelligence and Reasoning (LPAR-18)},
  pages =     {289-303},
  year =      2012,
  editor =    {Nikolaj Bj{\o}rner and Andrei Voronkov},
  volume =    {7180},
  series =    {LNCS},
  address =   {M{\'{e}}rida, Venezuela},
  publisher = {Springer},
}