Exercises

Below is a list of exercises, grouped by book chapter / section. Click on a chapter to browse through the related exercises.

2. First-Order Logic and Set Theory
   • Booleans
   • Propositional Logic
   • First-Order Logic
   • Set Theory
   • Functions and Relations
3. System Modelling
   • Finite State Machines
   • Defining Single Modules / Processes
   • Composition
   • Kripke Structures
   • Case Study
4. Functional System Properties in Temporal Logic
   • Safety vs. Liveness
   • Kripke Structures
   • LTL
   • Fairness
   • Fairness as an LTL Formula
   • CTL
   • Fairness and CTL
   • Comparison LTL / CTL
5. Model Checking Algorithms
   • CTL Model Checking
   • CTL Model Checking with Fairness
   • LTL Tableau
   • Safety Properties
   • Automata-Based LTL Model Checking
6. Analysing Software
   1. The Relation Between Code and Model
   2. Runtime Monitoring of Software
      • Runtime Monitoring in LarVa
      • Monitoring Time
      • Temporal Logic and LarVa
   3. Bounded Model Checking
      • Bounded Model Checking using CBMC
      • Modular Verification
   4. Bounded Symbolic Execution using CIVL
   5. Counter-Example-Guided Abstraction-Refinement
      • Predicate Abstraction
      • Boolean Programs
      • CEGAR Loop
   6. Automatic Test Suite Generation using CBMC
7. Design by Contract Specification Languages
   • Function Contracts
   • Pointer Specifications
   • Data Specifications
   • Multiple Function Behaviour
   • Inheritance
   • Exceptional Behaviour
8. Abstract Specifications
   • Functions in Contracts
   • Model Variables
   • Ghost Variables
9. Runtime Annotation Checking
   • Manual Validation
   • Executing Runtime Checker
   • Monitoring Behavioural Properties
10. Static Annotation Checking
    • Hoare Logic and Weakest Preconditions
    • Function Calls / Frames
    • Statement Annotations
    • Loop Invariants
    • Termination