Home

High-Level View

News

Industrial Use

Learning

The Toolbox

Tools

Advanced Topics

More Stuff

ccc

Advanced Topics

Leslie Lamport

Last modified on 27 June 2019


Introduction       [hide]

This page assumes you are familiar enough with TLA+ to be able to understand a simple TLA+ spec (not just a PlusCal spec).  It contains links to documents explaining topics that go beyond what most engineers need to know about TLA+.  These topics may be useful to engineers who want to push the boundary of what they can do with TLA+, and they will be of interest to those who want a deeper understanding of the principles underlying TLA+. 

Stuttering Steps       [show]

Safety, Liveness, and Fairness       [show]

Proving Safety Properties       [show]

Hiding, Refinement, and Auxiliary Variables       [show]