| 08:50 - 09:00 | Opening |
|---|---|
| 09:00 - 10:30 | Session 1 |
| 09:00 - 10:00 | Mechanical Software Verification: High Level Control Aspects from a User's Perspective (INVITED TALK) [abstract, ps] |
| Wolfgang Goerigk | |
| 10:00 - 10:30 | A Logic for Rewriting Strategies [abstract, ps] |
| Richard B. Kieburtz | |
| 10:30 - 11:00 | Coffee break |
| 11:00 - 12:30 | Session 2 |
| 11:00 - 11:30 | Termination of Rewriting with Local Strategies [abstract, ps] |
| Olivier Fissore, Isabelle Gnaedig and Hélène Kirchner | |
| 11:30 - 12:00 | An Algorithm for Guiding Clausal Temporal Resolution [abstract, ps] |
| M. Carmen Fernandez Gago, Michael Fisher and Clare Dixon | |
| 12:00 - 12:30 | Goal-Driven Inference Search in Classical Propositional Logic [abstract, ps] |
| Alexander Lyaletski and Andrey Paskevich | |
| 12:30 - 14:00 | Lunch break |
| 14:00 - 15:30 | Session 3 |
| 14:00 - 14:30 | A Pragmatic Approach to Reuse in Tactical Theorem Proving [abstract, ps] |
| Axel Schairer, Serge Autexier and Dieter Hutter | |
| 14:30 - 15:00 | A Proof-Planning Framework with Explicit Abstractions Based on Indexed Formulas [abstract, ps] |
| Serge Autexier | |
| 15:00 - 15:30 | Continuations of Proof Strategies [abstract, ps] |
| Julian Richardson and Alan Smaill | |
| 15:30 - 16:00 | Coffee break |
| 16:00 - 17:30 | Session 4 |
| 16:00 - 16:30 | Strategies for Interactive Proof and Program Development in Martin-Löf Type Theory (Extended Abstract) [abstract, ps] |
| Marcin Benke | |
| 16:30 - 17:30 | Final Discussion |