Model Checking IV

24 Novembro 2021, 16: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