* Examples
+ Verification of invariant properties
- IncDec System
- Mutual Exclusion Algorithm using test&set
- Mutual Exclusion Algorithm using Queue
- Mutual Exclusion Algorithm using atomicSwap
- Mutual Exclusion Algorithm using test&set Revisited
- Mutual Exclusion Algorithm using atomicSwap Revisited
- Simple Communication Protocol
- Alternating Bit Protocol
- NSLPK Authentication Protocol
- NSLPK Authentication Protocol Revisited

+ Verification of liveness properties
- Mutual Exclusion Algorithm using Queue (how to prove liveness properties)

+ Verification of realtime systems (invariants)
- Asynchronous Data Sending (realtime)
- Fischer's Protocol (realtime mutual exclusion algorithm)
- Railroad Crossing (realtime)

+ Verification of data
- Proof of (1 + ... + N) = N*(N + 1)/2
- Queue

* Gateaux: Proof Assistant of the OTS/CafeOBJ method
- Source in C
- Example 1 (Queuing Lock) using Gateaux
- Example 2 (NSLPK) usiing Gateaux

* Exercises
- Bank Account
- Mutual Exclusion Algorithm using atomicInc
- IFF Protocol