en
0.25
0.5
0.75
1.25
1.5
1.75
2
Model Checking and the Curse of Dimensionality
Published on Jul 10, 20125368 Views
Model Checking is an automatic verification technique for large state transition systems. It was originally developed for reasoning about finite-state concurrent systems. The technique has been used s
Related categories
Chapter list
Model Checking and the Curse of Dimensionality00:00
Turing's Quote on Program Verification01:02
Temporal Logic Model Checking01:51
Main Disadvantage (1)03:21
Main Disadvantage (2)04:20
Main Disadvantage (4)05:12
LTL - Linear Time Logic (Pn 77) (1)06:11
LTL - Linear Time Logic (Pn 77) (2)06:45
LTL - Linear Time Logic (Pn 77) (3)06:53
LTL - Linear Time Logic (Pn 77) (4)07:00
LTL - Linear Time Logic (Pn 77) (5)07:06
Branching Time (EC 80, BMP 81)07:13
CTL: Computation Tree Logic (1)07:53
CTL: Computation Tree Logic (2)08:44
CTL: Computation Tree Logic (3)09:05
CTL: Computation Tree Logic (4)09:29
CTL: Computation Tree Logic (5)09:46
Model Checking Problem10:18
Trivial Example11:52
Temporal Logic and Model Checking13:06
Model Checking14:14
Counterexamples (1)15:11
Counterexamples (2)16:21
Counterexamples (3)16:35
Hardware Example: IEEE Futurebus+16:49
Four Big Breakthroughs in Model Checking! (1)18:20
Four Big Breakthroughs in Model Checking! (3)20:23
Four Big Breakthroughs in Model Checking! (4)20:35
Four Big Breakthroughs in Model Checking! (5)22:24
Four Big Breakthroughs in Model Checking! (6)26:17
Existential Abstraction27:58
Preservation Theorem30:26
Spurious Behavior31:31
Automatic Abstraction33:49
CEGAR: CounterExample-Guided Abstraction Refinement35:10
Future Challenge: Is it possible to model check software?37:08
What Makes Software Model Checking Different? (1)38:03
What Makes Software Model Checking Different? (2)38:47
What Does It Mean to Model Check Software?39:21
Software Example: Device Driver Code40:06
Future Challenge: Can We Debug This Circuit? Kurt W.41:59
P53, DNA Repair, and Apoptosis42:20