en
0.25
0.5
0.75
1.25
1.5
1.75
2
Model Checking and the Curse of Dimensionality
Published on 2012-07-105378 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
Presentation
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