Presentation Schedule

Applications Session 1: Friday 22nd, 14:00-16:00
14:00-15:00 Invited Talk (shared with the Workshop on Disproving): Automatic Theorem Proving for Program Verification Engines
Byron Cook (Microsoft Research)
15:00-15:30 Practical Proof Checking for Program Certification
Geoff Sutcliffe, Ewen Denney, Bernd Fischer
15:30-16:00 Automated Theorem Proving for Quality-checking Medical Guidelines
Arjen Hommersom, Peter Lucas, Patrick van Bommel

Applications Session 2: Friday 22nd, 16:30-18:00
16:30-17:00 What First Order Theorem Provers Do For Monodic Temporal Reasoning
Michael Fisher, Ullrich Hustadt, Boris Konev, Alexei Lisitsa
17:00-17:30 MPTP 0.2: Design, Implementation, and First Cross-verification Experiments
Josef Urban
17:30-18:00 The Arrival of Automated Reasoning
Larry Wos, Matthew Spinks

Systems Session 1: Saturday 23rd, 09:00-10:00
09:00-10:00 Invited Talk: MiniSAT and some Applications of SAT
Niklas Sörensson (Chalmers University of Technology)

Systems Session 2: Saturday 23rd, 10:30-12:45
10:30-11:00 Tau: A Web-Deployed Hybrid Prover for First-Order Logic with Identity, with Optional Inductive Proof
Jay Halcomb, Randall Schulz
11:00-11:30 The Implementation of Logiweb
Klaus Grue
11:30-12:00 Things to know when implementing KBO
Bernd Löchner
12:00-12:30 Panel: What Tools and Structures are Needed for more Empirically Successful Classical Automated Reasoning?
Panelists: Byron Cook, John Slaney, Andrei Voronkov
12:30-12:45 Best Paper Award