Sumários
Model Checking III
29 Novembro 2023, 16:30 • Antónia Lopes
Model Checking III
- Safety and Liveness properties
- Verification of LTL properties with Spin
- Never claims
- Modelling communicating processes
- Rendez-vous channels
- Buffered channels
Model Checking II
22 Novembro 2023, 16:30 • Antónia Lopes
Model Checking II
- Concurrency
- Synchronisation
- Linear Temporal Logic
- Syntax and semantics
Model Checking I
15 Novembro 2023, 16:30 • Antónia Lopes
Model Checking
- Introduction
- Modelling sequential programs in Promela
- Specifying properties with assertions in Promela
- Verifying sequential programs with Spin