8:50 - 9:00 | |
| |
09:00 - 09:50 | |
09.50 - 10:30 |
|
10:30 - 11:00 | |
| |
11:00 - 11:50 | |
11:50 - 12:30 |
|
12:30 - 01:40 | |
| |
01:40 - 02:30 | |
02:30 - 03:30 |
|
03:30 - 04:00 | |
| |
04:00 - 05:20 |
|
05:20 - 05:50 | |
This is joint work with Toby Hu. |
[Joint work with Ron Parr, David Andre, Bhaskara Marthi, Andy Zimdars, David Latham, Carlos Guestrin, Jason Wolfe] |
Symbolic Model Checking (SMC) is a formal technique for ensuring functional correctness, that is achieving increasing industrial penetration. In this talk, we show how SMC can be used as a convenient framework for safety analysis, planning and plan validation, diagnosis and diagnosability, and monitoring. We also discuss how advanced model checking tools, based on Satisfiability Modulo Theory solvers, can be used to address the resulting computational challenges. |