Formalization of the GPS program logic
Version 1.7, released 2016-12-20
Copyright © Viktor Vafeiadis
Copyright © Viktor Vafeiadis
- C11 concurrency model definition
- Program expressions and their semantics
- B.2. Semantic structures
- B.3. Local safety
- B.4. Global safety
- B.5. Syntax and semantics
- B.6. Proof theory
- C.3.1. Visibility
- C.3.2. Rely
- C.3.3. Ghost moves
- C.3.4. Protocol equivalence for writes
- C.3.5. Guarantee
- C.3.6. Prepare
- C.3.7. Instrumented execution and adequacy
This page has been generated by coqdoc