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.