Verifying Safety Properties With the TLA+ Proof System

Details Verifying Safety Properties With the TLA+ Proof System Verifying Safety Properties With the TLA+ Proof System

2010-11-11

arxiv.org/abs/1011.2560v1

Fifth International Joint Conference on Automated Reasoning (IJCAR), Edinburgh : United Kingdom (2010)

Computer Science

Logic in Computer Science

Scientific paper

10.1007/978-3-642-14203-1_12

TLAPS, the TLA+ proof system, is a platform for the development and mechanical verification of TLA+ proofs written in a declarative style requiring 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. A Proof Manager uses backend verifiers such as theorem provers, proof assistants, SMT solvers, and decision procedures to check TLA+ proofs. This paper documents the first public release of TLAPS, 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.

Affiliated with

Also associated with

No associations

Rating

Verifying Safety Properties With the TLA+ Proof System does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with Verifying Safety Properties With the TLA+ Proof System, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Verifying Safety Properties With the TLA+ Proof System will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-430479