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