- Concurrent algorithm typically described by a program.
- Correctness of algorithm means program satisfies desired
- TLA = Temporal Logic of Actions.
- Lamport, 1994.
- Both algorithm and property are specified by formulas in single logic.
- Correctness of algorithm means algorithm implies property.
- Reasonable to abandon programing language?
- Mostly reasoning about concurrent algorithms.
- Concurrent programs are much to complicated.
- 1 page algorithm = 5000 lines of C code.
- Goal to detect algorithmic errors.
Talking about concurrent algorithms!
Author: Wolfgang Schreiner
Last Modification: May 14, 1998