Sumários
Model Checking IV
7 Dezembro 2022, 18:30 • Antónia Lopes
- Exploring the search space in presence of an LTL formula
- Never claims for a safety properties
- Never claims for a liveness properties
- Optimizing the performance of verifications
- The sources of complexity of model checking
- Write efficient models
- Understand how Spin allocates memory for the hash table
- Compress the state vector
- Bitstate hashing
- Use a minimal automaton
Model Checking III
7 Dezembro 2022, 16:30 • Antónia Lopes
Modelling different protocols in Promela and verify properties in LTL with Spin.
Solved exercises: 5.11, 5.13
Model Checking II
30 Novembro 2022, 18:30 • Antónia Lopes
Modelling sequential and concurrent systems in Promela. Specification of properties with assertions and linear temporal logic and their verification with Spin.
Exercises solved in class: 5.6, 5.9, 5.10