TLA + Proofs

DOI10.1007/978-3-642-32759-9_14MaRDI QIDQ4647839zbMATH OpenOpenAlexFDO

Authors Denis Cousineau, Damien Doligez, Leslie Lamport, Stephan Merz, Daniel Ricketts, Hernán Vanzetto

Publication date 8 November 2012

Published in FM 2012: Formal Methods (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1208.5933, https://hal.inria.fr/hal-00726631/file/final.pdf

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Abstract: TLA+ is a specification language based on standard set theory and temporal logic that has constructs for hierarchical proofs. We describe how to write TLA+ proofs and check them with TLAPS, the TLA+ Proof System. We use Peterson's mutual exclusion algorithm as a simple example to describe the features of TLAPS and show how it and the Toolbox (an IDE for TLA+) help users to manage large, complex proofs.

Recommendations

• scientific article; zbMATH DE number 2172804
• T-theorem proving. I
• Frege proof system and TNC°
• Lower Bounds of Static Lovász-Schrijver Calculus Proofs for Tseitin Tautologies
• scientific article; zbMATH DE number 5161489
• scientific article; zbMATH DE number 1670575
• Proof-theoretic aspects of the Lambek-Grishin calculus
• An intuitionistic proof of Tychonoff's theorem
• scientific article; zbMATH DE number 910717
• scientific article; zbMATH DE number 2185692

Cited in

(12)

• scientific article; zbMATH DE number 1390253 (Why is no real title available?)
• A deductive approach towards reasoning about algebraic transition systems
• Improving automation for higher-order proof steps
• The PlusCal Algorithm Language
• A case study on parametric verification of failure detectors
• scientific article; zbMATH DE number 2172804 (Why is no real title available?)
• scientific article; zbMATH DE number 2064460 (Why is no real title available?)
• Reconstruction of SMT proofs with Lambdapi
• Certification of an exact worst-case self-stabilization time
• Automatic verification of TLA\(^{ + }\) proof obligations with SMT solvers
• Towards an automatic proof of the bakery algorithm
• Formal proof of a machine closed theorem in Coq

Describes a project that uses

Uses Software

• TLAPS

This page was built for publication: TLA +  Proofs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4647839)