| 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
| | | |