Sumários

Model Checking III

30 Novembro 2022, 16:30 • Antónia Lopes

  • Linear Temporal Logic
    • Syntax and semantics
    • Safety and Liveness properties
    • Verification of LTL properties with Spin
  • Modelling communicating processes that exchange messages through buffered channels or use rendezvous points in Promela

Model Checking I

23 Novembro 2022, 18:30 • Antónia Lopes

Modelling sequential and concurrent systems in Promela. Specification of properties with assertions and verification with Spin.

Exercises solved in class: 5.3, 5.4, 5.5

Model Checking II

23 Novembro 2022, 16:30 • Antónia Lopes

  • Modelling concurrent programs in Promela
    • The interleaving model
    • Modelling atomicity
    • The critical section problem
    • Synchronization
    • Deadlocks and Termination
    • How assertions are verified

Design by Contract in Dafny

16 Novembro 2022, 18:30 • Antónia Lopes

Writing classes in Dafny with property-based specifications

Exercises solved in class: 4.3

Model Checking I

16 Novembro 2022, 16:30 • Antónia Lopes


  • Introduction
  • Modelling sequential programs in Promela
  • Specifying properties with assertions in Promela
  • Verifying sequential programs with Spin