Model Checking IV

26 Novembro 2025, 16:30 • Antónia Lopes

• More about channels in Promela
• Variants of Model Checking
• How Spin searches the space state
• Optimizing the performance of verifications

---

Exercises Spin

19 Novembro 2025, 18:30 • Antónia Lopes

Exercises5 (Spin): 5.9, 5.10, 5.6 (revisited)

---

Model Checking III

19 Novembro 2025, 16:30 • Antónia Lopes

• Linear Temporal Logic
  • Safety and Liveness properties
  • Fairness
• Verification of LTL properties with Spin
  • Never claims
•  Modelling communicating processes
  • Rendez-vous channels
  • Buffered channels

---

Exercises Spin

12 Novembro 2025, 18:30 • Antónia Lopes

Exercises5 (Spin): 5.3, 5.5, 5.6

---

Model Checking II

12 Novembro 2025, 16:30 • Antónia Lopes

• Concurrency
  • Interleaving model
  • Atomicity
  • Synchronisation
  • Examples addressing the mutual exclusion problem

---