Program

All sessions will take place in Richmond unless otherwise indicated.

Wednesday, August 16th

Wednesday's program is also available with abstracts or side by side with other meetings.

09:00‑10:00  Invited Talk

09:00

Jian Zhang (Institute of Software, Chinese Academy of Sciences) Model and Counterexample Search: Successes and Challenges [pdf]

10:00‑10:30  Session 1: Base technology

10:00

Thomas Hillenbrand , Dalibor Topic and Christoph Weidenbach Sudokus as Logical Puzzles

10:30‑11:00  Break

11:00‑11:30  Session 2: Base technology

11:00

André Rognes Automated relative consistency proving

11:30‑12:30  Session 3: Verification

11:30	Lee Pike , Paul Miner and Wilfredo Torres-Pomales Diagnosing a Failed Proof in Fault-Tolerance: A Disproving Challenge Problem
12:00	Markus Aderhold , Christoph Walther , Daniel Szallies and Andreas Schlosser A Fast Disprover for VeriFun

12:30‑14:00  Lunch break

14:00‑15:00  Invited Talk

14:00

Silvio Ranise (LORIA-INRIA-Lorraine & Università degli Studi di Milano) Satisfiability Solving for Program Verification: towards the efficient combination of Automated Theorem Provers and Satisfiability Modulo Theory Tools [pdf]

15:00‑15:30  Session 4: Verification

15:00

Louise Abigail Dennis Program Slicing and Middle-Out Reasoning for Error Location and Repair

15:30‑16:00  Break

16:00‑17:00  Session 5: Base Technology

16:00	Mahadevan Subramaniam, Deepak Kapur and Stephan Falke Predicting Failures of Inductive Proof Attempts
16:30	Peter Baumgartner , Alexander Fuchs , Cesare Tinelli and Hans de Nivelle Computing Finite Models by Reduction to Function-Free Clause Logic