TY - GEN
T1 - Verifying safety properties with the TLA+ proof system
AU - Chaudhuri, Kaustuv
AU - Doligez, Damien
AU - Lamport, Leslie
AU - Merz, Stephan
PY - 2010/8/10
Y1 - 2010/8/10
N2 - TLAPS, the TLA+ proof system, is a platform for the development and mechanical verification of TLA+ proofs. The TLA+ proof language is declarative, and understanding proofs requires little background beyond elementary mathematics. The language supports hierarchical and non-linear proof construction and verification, and it is independent of any verification tool or strategy. Proofs are written in the same language as specifications; engineers do not have to translate their high-level designs into the language of a particular verification tool. A proof manager interprets a TLA+ proof as a collection of proof obligations to be verified, which it sends to backend verifiers that include theorem provers, proof assistants, SMT solvers, and decision procedures. The first public release of TLAPS is available from [1], distributed with a BSD-like license. It handles almost all the non-temporal part of TLA+ as well as the temporal reasoning needed to prove standard safety properties, in particular invariance and step simulation, but not liveness properties. Intuitively, a safety property asserts what is permitted to happen; a liveness property asserts what must happen; for a more formal overview, see [3,10].
AB - TLAPS, the TLA+ proof system, is a platform for the development and mechanical verification of TLA+ proofs. The TLA+ proof language is declarative, and understanding proofs requires little background beyond elementary mathematics. The language supports hierarchical and non-linear proof construction and verification, and it is independent of any verification tool or strategy. Proofs are written in the same language as specifications; engineers do not have to translate their high-level designs into the language of a particular verification tool. A proof manager interprets a TLA+ proof as a collection of proof obligations to be verified, which it sends to backend verifiers that include theorem provers, proof assistants, SMT solvers, and decision procedures. The first public release of TLAPS is available from [1], distributed with a BSD-like license. It handles almost all the non-temporal part of TLA+ as well as the temporal reasoning needed to prove standard safety properties, in particular invariance and step simulation, but not liveness properties. Intuitively, a safety property asserts what is permitted to happen; a liveness property asserts what must happen; for a more formal overview, see [3,10].
U2 - 10.1007/978-3-642-14203-1_12
DO - 10.1007/978-3-642-14203-1_12
M3 - Conference contribution
AN - SCOPUS:77955264460
SN - 3642142028
SN - 9783642142024
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 142
EP - 148
BT - Automated Reasoning - 5th International Joint Conference, IJCAR 2010, Proceedings
T2 - 5th International Joint Conference on Automated Reasoning, IJCAR 2010
Y2 - 16 July 2010 through 19 July 2010
ER -