TLA+ Proofs
Overview & Synopsis
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 \tlaplus Proof System. We use Peterson's mutual exclusion algorithm as a simple example and show how TLAPS and the Toolbox (an IDE for TLA+) help users to manage large, complex proofs.
Indexed from repository: HAL Open Science
(
hal.science)
Keyboard Shortcuts:
← / → for pages • + / - for zoom • 0 to fit width
Powered by Mozilla PDF.js v3.11
Document Information
| Document Title | TLA+ Proofs |
|---|---|
| Author / Organization | Denis Cousineau, Damien Doligez, Leslie Lamport, Stephan Merz, Daniel Ricketts, Hernán Vanzetto |
| Subject & Discipline | Multidisciplinary Academic Open Research |
| Categories | Science & Mathematics |
| Publication Year | 2012 |
| License / Rights | Open Access / Creative Commons |
| Resource Verification | Listed PDF (Verification Pending) |
| Original Host Website |
HAL Open Science
(hal.science)
|
| File Format | application/pdf (Portable Document Format) |
| Language | EN |
| Catalog ID | DOC-226974 |
| Original Source Link | Visit Source Page on hal.science » |