Model Checking IV

5 Dezembro 2017, 18:30 Vasco Manuel Thudichum de Serpa Vasconcelos

  • Explicit-state model checking of LTL properties
    • Buchi automata
    • From LTL to Buchi automata
    • Reduction to an emptiness problem
  • How to control the state-explosion problem in SPIN
    • Storage of states
    • State Compression 
    • State representation
    • Partial order reduction