| 8:30 |
Continental Breakfast
Location: Training Room D |
|
| 9:00 |
Welcome and Introductions |
Natasha Sharygina, Carnegie Mellon University |
| 9:15 |
Welcome and Background |
Ed Clarke, CMU |
| 9:30 |
On-the-fly Independence in Bogor: Partial Order Reductions for Dynamic Software |
Matthew Dwyer, Kansas State University |
| 10:15 |
Specifying and Verifying Concurrent C Programs by MAGIC |
Sagar Chaki, Carnegie Mellon University |
| 11:00 |
Break |
|
| 11:15 |
Lessons Learned From Verification of a NASA Robot Controller |
James C. Browne, The University of Texas at Austin |
| 12:00 |
Lunch
Location: Training Room D |
|
| 13:00 |
Predicate Abstraction of ANSI-C Programs using SAT |
Karen Yorav, Carnegie Mellon University |
| 13:45 |
The Java PathFinder Experience |
Willem Visser, NASA Ames |
| 14:30 |
Break |
|
| 15:00 |
Behavioral Consistency of C and Verilog Programs Using Bounded Model Checking |
Daniel Kroening, Carnegie Mellon University |
| 15:45 |
Calvin: a modular checker for multithreaded Java programs |
Shaz Qadeer, Microsoft Research |
| 16:30 |
Discussions |
|
| 17:15 |
Conclusions and next steps |
|
| 19:00 |
Dinner |
|