Model Checking II

10 Novembro 2021, 16:30 • Antónia Lopes

Model Checking

• Modelling concurrent programs in Promela
  • The critical section problem
  • Synchronization
  • Termination
• Linear Temporal Logic
• Verification  with Linear Temporal Logic in Spin