出版社：European Association of Software Science and Technology (EASST)
摘要：TLA + is a language based on Zermelo-Fraenkel set theory and linear temporal logic designed for specifying and verifying concurrent and distributed al- gorithms and systems. The TLA + proof system TLAPS allows users to interactively verify safety properties of these systems. At the core of TLAPS , a proof manager interprets the proof language, generates corresponding proof obligations and passes them to backend provers. We recently developed a backend that relies on a typing discipline to encode (untyped) TLA + formulas into multi-sorted first-order logic for SMT solvers. In this paper we present a different encoding of TLA + formulas that does not require explicit type inference for TLA + expressions. We also present a number of techniques based on rewriting in order to simplify the resulting formulas.
