Scientific Program
The scientific program consists of the following talks:
Alois Altendorfer | Case Studies in Proof Based Synthesis of Unification Algorithms | RISC |
Serge Autexier and Dominik Dietrich | A Tactic Language for Declarative Proofs | DFKI |
Serge Autexier and Normen Müller | Semantics-Based Change Impact Analysis for Heterogeneous Collections of Documents | DFKI |
Bruno Buchberger | Where we stand | RISC |
Alan Bundy | Equation Solving in Recursive Theories | Edinburgh |
Lucas Dixon | Reasoning and Representation with Graphs | Edinburgh |
Isabela Dramnesc | Case Studies in Proof Based Synthesis of Sorting Algorithms | RISC |
Madalina Erascu | Imperative Program Verification | RISC |
Lilia Georgieva | Synthesis of decision procedures | Edinburgh |
Dieter Hutter | Patching Security Protocols with Type Flaws | DFKI |
Tudor Jebelean | Overview of Program Verification and Synthesis in Theorema | RISC |
Temur Kutsia | Order-sorted Unification with Regular Expression Sorts | RISC |
Christoph Lüth | Querying HiProofs | DFKI |
Roy McCasland | Theorem-Producing Rules: Two Years on | Edinburgh |
Nikolaj Popov | Functional Program Verification | RISC |
Omar Montano Rivas | Scheme-based Synthesis of Inductive Theories | Edinburgh |
Alan Smaill | Computing blends of theories | Edinburgh |
Nathan Wasser | Partial C- and ACI-Pattern-Matching | Darmstadt |
Iain Whiteside | Refactoring Interactive Proof | Edinburgh |
Wolfgang Windsteiger | Theorema2: Some Design Cosiderations for the Re-Implementation of the Theorema System | RISC |
A preliminary schedule is available.