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