Chapter outline

The following is the course table of contents for the book (source: book-chapters.md next to this project).

Course book¶

Table of contents¶

Part 1: Formal specification (Chapters 1 & 2)¶

1. System specification with TLA+/PlusCal

2. Relational modeling with Alloy

Part 2: Static Analysis & Model Checking (Chapters 4–5)¶

3. Model checking with nuXmv/NuSMV

4. Timed model checking with UPPAAL

5. Program analysis in Dafny

Part 3: Proof assistants & dependent types (Chapters 6–9)¶

6. Proof and verification in Lean

7. Effectful programming in Haskell

8. Program extraction with Rocq

Part 4: Probabilistic and quantum methods (Chapter 9-11)¶

9. Probabilistic model checking with PRISM

10. Quantum programming with Qiskit

11. Quantum circuit verification with PyZX

Each chapter should be based on the following sectioning:

1. Idea

2. Basic theory

3. History

[ ... ] Further subsections containing the specific materials [...]

n. References