| 08:55-9:00 |
Welcome |
| |
Brigitte Pientka (Conference Chair) |
| 09:00-10:00 |
Session 1: Invited Talk Chair: Aaron Stump |
| |
Integrated Reasoning and Proof Choice Point Selection in the Jahob System: Mechanisms for Program Survival |
| |
Martin Rinard |
|
10:00-10:30 |
Coffee Break |
| 10:30-12:30 |
Session 2: Combinations
and Extensions Chair: Nikolaj Bjørner |
| 10:30 |
Superposition and Model Evolution Combined |
| |
Peter Baumgartner and Uwe Waldmann |
|
11:00 |
On Deciding Satisfiability by DPLL(
) and Unsound Theorem Proving |
| |
Maria Paola Bonacina, Christopher Lynch and Leonardo de Moura |
|
11:30 |
Combinable Extensions of Abelian Groups |
| |
Enrica Nicolini, Christophe Ringeissen and Michaël Rusinowitch |
|
12:00 |
Locality Results for Certain Extensions of Theories with Bridging Functions |
| |
Viorica Sofronie-Stokkermans |
|
12:30-14:00 |
Catered Lunch |
| 14:00-15:30 |
Session 3: Minimal Unsatisfiability and Automated Reasoning Support Chair: Carsten Schürmann |
| 14:00 |
Axiom Pinpointing in Lightweight Description Logics via Horn-SAT Encoding and Conflict Analysis |
| |
Roberto Sebastiani and Michele Vescovi |
|
14:30 |
Does this Set of Clauses Overlap with at least one MUS? |
| |
Éric Grégoire, Bertrand Mazure and Cédric Piette |
|
15:00 |
Progress in the Development of Automated Theorem Proving for Higher-Order Logic |
| |
Geoff Sutcliffe, Christoph Benzmüller, Chad E. Brown and Frank Theiss |
|
15:30-16:00 |
Coffee Break |
| 16:00-17:40 |
Session 4: System Descriptions Chair: Peter Baumgartner |
| 16:00 |
System Description: H-PILoT |
| |
Carsten Ihlemann and Viorica Sofronie-Stokkermans |
|
16:20 |
SPASS Version 3:5 |
| |
Christoph Weidenbach, Dilyana Dimova, Arnaud Fietzke, Rohit Kumar, Martin Suda and Patrick Wischnewski |
|
16:40 |
DEI: A Theorem Prover for Terms with Integer Exponents |
| |
Hicham Bensaid, Ricardo Caferra and Nicolas Peltier |
|
17:00 |
veriT: An Open, Trustable and Efficient SMT-Solver |
| |
Thomas Bouton, Diego Caminha B. de Oliveira, David Déharbe and Pascal Fontaine |
|
17:20 |
Divvy: An ATP Meta-system Based on Axiom Relevance Ordering |
| |
Alex Roederer, Yury Puzis and Geoff Sutcliffe |
|
17:40-17:50 |
Handover of Festschrift to Peter B. Andrews |
| |
Christoph Benzmüller (Co-Editor) |
| 17:50-19:00 |
CADE Business Meeting |
| |
Reiner Hähnle (Vice-President) |
| 09:00-10:00 |
Session 5: Invited Talk Chair: Cesare Tinelli |
| |
Instantiation-Based Automated Reasoning: From Theory to Practice |
| |
Konstantin Korovin |
|
10:00-10:30 |
Coffee Break |
| 10:30-12:30 |
Session 6: Interpolation and Predicate Abstraction |
| |
Chair: Maria Paola Bonacina |
| 10:30 |
Interpolant Generation for UTVPI |
| |
Alessandro Cimatti, Alberto Griggio and Roberto Sebastiani |
|
11:00 |
Ground Interpolation for Combined Theories |
| |
Amit Goel, Sava Krstic and Cesare Tinelli |
|
11:30 |
Interpolation and Symbol Elimination |
| |
Laura Kovács and Andrei Voronkov |
|
12:00 |
Complexity and Algorithms for Monomial and Clausal Predicate Abstraction |
| |
Shuvendu K. Lahiri and Shaz Qadeer |
|
12:30-14:00 |
Catered Lunch |
| 14:00-15:30 |
Session 7: Resolution-Based Systems for Non-classical Logics Chair: Hans de Nivelle |
| 14:00 |
Efficient Intuitionistic Theorem Proving with the Polarized Inverse Method |
| |
Sean McLaughlin and Frank Pfenning |
|
14:30 |
A Refined Resolution Calculus for CTL |
| |
Lan Zhang, Ullrich Hustadt and Clare Dixon |
|
15:00 |
Fair Derivations in Monodic Temporal Reasoning |
| |
Michel Ludwig and Ullrich Hustadt |
|
15:30-16:00 |
Coffee Break |
| 16:00-17:00 |
Session 8: Termination Analysis and Constraint Solving |
| |
Chair: Christopher Lynch |
| 16:00 |
A Term Rewriting Approach to the Automated Termination Analysis of Imperative Programs |
| |
Stephan Falke and Deepak Kapur |
|
16:30 |
Solving Non-linear Polynomial Arithmetic via SAT Modulo Linear Arithmetic |
| |
Cristina Borralleras, Salvador Lucas, Rafael Navarro-Marset, Enric Rodríguez-Carbonell and Albert Rubio |
|
17:00-18:00 |
Presentation of the Herbrand Award to Deepak Kapur |
| |
Reiner Hähnle (Master of Ceremony) |
| 09:00-10:00 |
Session 9: Invited Talk Chair: Geoff Sutcliffe |
| |
Building Theorem Provers |
| |
Mark E. Stickel |
|
10:00-10:30 |
Coffee Break |
| 10:30-12:30 |
Session 10: Rewriting, Termination and Productivity |
| |
Chair: Christoph Weidenbach |
| 10:30 |
Termination Analysis by Dependency Pairs and Inductive Theorem Proving |
| |
Stephan Swiderski, Michael Parting, Jürgen Giesl, Carsten Fuhs and Peter Schneider-Kamp |
|
11:00 |
Beyond Dependency Graphs |
| |
Martin Korp and Aart Middeldorp |
|
11:30 |
Computing Knowledge in Security Protocols under Convergent Equational Theories |
| |
Stefan Ciobâca, Stéphanie Delaune and Steve Kremer |
|
12:00 |
Complexity of Fractran and Productivity |
| |
Jörg Endrullis, Clemens Grabmayer and Dimitri Hendriks |
|
12:30-14:00 |
Catered Lunch |
| 14:00- |
Excursion and Banquet at Pointe-à-Callière |
| 09:00-10:00 |
Session 11: Models Chair: Albert Oliveras |
| 09:00 |
Automated Inference of Finite Unsatisfiability |
| |
Koen Claessen and Ann Lillieström |
|
09:30 |
Decidability Results for Saturation-Based Model Building |
| |
Matthias Horbach and Christoph Weidenbach |
|
10:00-10:30 |
Coffee Break |
| 10:30-11:30 |
Session 12: Modal Tableaux with Global Caching |
| |
Chair: Ullrich Hustadt |
| 10:30 |
A Tableau Calculus for Regular Grammar Logics with Converse |
| |
Linh Anh Nguyen and Andrzej Szałas |
|
11:00 |
An Optimal On-the-fly Tableau-Based Decision Procedure for PDL-Satisfiability |
| |
Rajeev Goré and Florian Widmann |
|
11:30-12:30 |
System Competition Results Chair: Renate Schmidt |
| 11:30 |
CASC: The CADE ATP System Competition |
| |
Geoff Sutcliffe |
| 12:00 |
SMT-COMP: Satisfiability Modulo Theories Competition |
| |
Albert Oliveras |
| 12:30-14:00 |
Catered Lunch |
| 14:00-15:30 |
Session 13: Arithmetic Chair: Reiner Hähnle |
| 14:00 |
Volume Computation for Boolean Combination of Linear Arithmetic Constraints |
| |
Feifei Ma, Sheng Liu and Jian Zhang |
|
14:30 |
A Generalization of Semenov's Theorem to Automata over Real Numbers |
| |
Bernard Boigelot, Julien Brusten and Jérôme Leroux |
|
15:00 |
Real World Verification |
| |
André Platzer, Jan-David Quesel and Philipp Rümmer |
|
15:30-16:00 |
Coffee Break |