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 |