| Time | Title | Place |
|---|
| 9:00-10:00 |
Session 9: Invited Talk |
Rainer Haehnle |
| 9:00-10:00 |
Designing Verification Conditions for Software |
K. Rustan M. Leino |
| 10:00-10:30 |
Coffee Break |
|
| 10:30-12:30 |
Session 10: Model Checking and Verification |
Cesare Tinelli |
| 10:30-11:00 |
Encodings of Bounded LTL Model Checking in Effectively Propositional Logic |
Juan Antonio Navarro Perez, Andrei Voronkov |
| 11:00-11:30 |
Combination Methods for Satisfiability and Model-Checking of Infinite-State Systems |
Silvio Ghilardi, Enrica Nicolini, Silvio Ranise, Daniele Zucchelli |
| 11:30-11:45 |
The KeY System |
Bernhard Beckert, Martin Giese, Reiner H¨ahnle, Vladimir Klebanov,
Philipp Ruemmer, Steffen Schlager, Peter H. Schmitt |
| 11:45-12:00 |
KeY-C: A Tool for Verification of C Programs |
Oleg Muerk, Daniel Larsson, Reiner Haehnle |
| 12:00-12:15 |
The Bedwyr system for model checking over syntactic expressions |
David Baelde, Andrew Gacek, Dale Miller, Gopalan Nadathur, Alwen Tiu |
| 12:15-12:30 |
System for Automated Deduction (SAD): a Tool for Proof Verification |
Konstantin Verchinine, Alexander Lyaletski, Andrei Paskevich |
| 12:30-14:00 |
Lunch Break |
|
| 14:00-18:00 |
CADE Excursions |
|
| 18:00-23:00 |
CADE Conference Dinner |
Schiffahrtsmuseum Bremerhaven |