Friday, July 16th
Friday's program is also available with abstracts and side by side with other events.
09:00‑10:00 FLoC Plenary Talk: David Basin
Location: George Square Lecture Theatre
| 09:00 | David Basin (ETH Zurich) Policy Monitoring in First-order Temporal Logic |
10:30‑12:30 Logical Frameworks & Combination of Systems
Location: AT LT5
| 10:30 | Mike Gordon (University of Cambridge) Remembering Robin Milner |
| 10:45 | Anders Schack-Nielsen and Carsten Schürmann Curry-Style Explicit Substitutions for the Linear and Affine Lambda Calculus |
| 11:15 | Brigitte Pientka and Joshua Dunfield Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description) |
| 11:30 | Silvio Ghilardi and Silvio Ranise MCMT: A Model Checker Modulo Theories |
| 11:45 | Carsten Ihlemann and Viorica Sofronie-Stokkermans On efficient reasoning in combinations of theories |
14:00‑15:00 Description Logic I
Location: AT LT5
| 14:00 | Rajeev Goré, Clemens Kupke, Dirk Pattinson and Lutz Schröder Global Caching for Coalgebraic Description Logics |
| 14:30 | Despoina Magka, Yevgeny Kazakov and Ian Horrocks Tractable Extensions of the Description Logic EL with Numerical Datatypes |
15:30‑17:00 Higher-Order Logic
Location: AT LT5
| 15:30 | Julian Backes and Chad Brown Analytic Tableaux for Higher-Order Logic with Choice |
| 16:00 | Jasmin Christian Blanchette and Alexander Krauss Monotonicity Inference for Higher-Order Formulas |
| 16:30 | Sascha Böhme and Tobias Nipkow Sledgehammer: Judgement Day |
Saturday, July 17th
Saturday's program is also available with abstracts and side by side with other events.
09:00‑10:00 Invited Talk
Location: AT LT5
| 09:00 | Johan van Benthem (Stanford University and University of Amsterdam) Logic between Expressivity and Complexity |
10:30‑12:30 Verification
Location: AT LT5
| 10:30 | Ali Ayad and Claude Marché Multi-Prover Verification of Floating-Point Programs |
| 11:00 | Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport and Stephan Merz Verifying Safety Properties With the TLA+ Proof System |
| 11:15 | Ruzica Piskac and Viktor Kuncak MUNCH - Automated Reasoner for Sets and Multisets |
| 11:30 | Elena Sherman, Brady J. Garvin and Matthew B. Dwyer A Slice-based Decision Procedure for Type-based Partial Orders |
| 12:00 | Viorica Sofronie-Stokkermans Hierarchical reasoning for the verification of parametric systems |
14:00‑15:00 First-Order Logic
Location: AT LT5
| 14:00 | Krystof Hoder, Laura Kovacs and Andrei Voronkov Symbol Elimination and Interpolation in Vampire |
| 14:15 | Konstantin Korovin and Christoph Sticksel iProver-Eq: An Instantiation-based Theorem Prover with Equality |
| 14:30 | Hans de Nivelle Classical Logic with Partial Functions |
15:30‑17:00 Non-Classical Logic
Location: AT LT5
| 15:30 | Christoph Beierle, Marc Finthammer, Gabriele Kern-Isberner and Matthias Thimm Automated Reasoning for Relational Probabilistic Knowledge Representation |
| 15:45 | Rajeev Goré and Florian Widmann Optimal Tableaux for Propositional Dynamic Logic with Converse |
| 16:15 | Mark Kaminski and Gert Smolka Terminating Tableaux for Hybrid Logic with Eventualities |
| 16:45 | Marta Cialdea Mayer and Serenella Cerrito Herod and Pilate: two tableau provers for basic hybrid logic |
17:10‑18:30 Business Meetings (held at Forum building)
Location: AT LT5
| 17:10 | CADE Business Meeting |
| 17:50 | Tableaux Business Meeting |
Sunday, July 18th
Sunday's program is also available with abstracts and side by side with other events.
09:00‑10:00 Induction
Location: AT LT5
| 09:00 | Markus Aderhold Automated Synthesis of Induction Axioms for Programs with Second-Order Recursion |
| 09:30 | David Baelde, Dale Miller and Zachary Snow Focused Inductive Theorem Proving |
10:30‑12:30 Decision Procedures
Location: AT LT5
| 10:30 | Vincent Aravantinos, Ricardo Caferra and Nicolas Peltier A Decidable Class of Nested Iterated Schemata |
| 11:00 | Vincent Aravantinos, Ricardo Caferra and Nicolas Peltier RegSTAB: a SAT-Solver for Propositional Schemata |
| 11:15 | Nikolaj Bjørner Linear Quantifier Elimination as an Abstract Decision Procedure |
| 11:45 | Oliver Friedmann, Markus Latte and Martin Lange A Decision Procedure for CTL* Based on Tableaux and Automata |
| 12:15 | Filip Maric and Predrag Janicic URBiVA: Uniform Reduction to Bit-Vector Arithmetic |
14:00‑15:00 FLoC Keynote Talk: Deepak Kapur
Location: George Square Lecture Theatre
| 14:00 | Deepak Kapur (University of New Mexico) Induction, Invariants, and Abstraction |
15:30‑17:00 Arithmetic
Location: AT LT5
| 15:30 | Jonathan Abourbih, Luke Blaney, Alan Bundy and Fiona McNeill A Single-Significant-Digit Calculus for Semi-Automated Guesstimation |
| 16:00 | Hicham Bensaid, Ricardo Caferra and Nicolas Peltier Perfect discrimination graphs: indexing terms with integer exponents |
| 16:30 | Angelo Brillout, Daniel Kroening, Philipp Rümmer and Thomas Wahl An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic |
Monday, July 19th
Monday's program is also available with abstracts and side by side with other events.
09:00‑10:00 Invited Talk
Location: AT LT5
| 09:00 | Leonardo de Moura (Microsoft Research Redmond) Bugs, Moles and Skeletons: Symbolic Reasoning for Software Development |
10:30‑12:00 Applications
Location: AT LT5
| 10:30 | Vincent Cheval, Hubert Comon-Lundh and Stephanie Delaune Automating security analysis: symbolic equivalence of constraint systems |
| 11:00 | Cvetan Dunchev, Alexander Leitsch, Tomer Libal, Daniel Weller and Bruno Woltzenlogel Paleo The Proof Transformation System CERES |
| 11:15 | Daniel Kühlwein, Marcos Cramer, Peter Koepke and Bernhard Schröder Premise Selection in the Naproche System |
| 11:30 | Martin Suda, Christoph Weidenbach and Patrick Wischnewski On the Saturation of YAGO |
| 12:00 | Geoff Sutcliffe Results of the CASC-J5 System Competition |
14:00‑15:00 Description Logic II
Location: AT LT5
| 14:00 | Birte Glimm, Ian Horrocks and Boris Motik Optimized Description Logic Reasoning via Core Blocking |
| 14:30 | Yevgeny Kazakov An Extension of Complex Role Inclusion Axioms in the Description Logic SROIQ |
15:30‑17:30 Termination
Location: AT LT5
| 15:30 | Nao Hirokawa and Aart Middeldorp Decreasing Diagrams and Relative Termination |
| 16:00 | Friedrich Neurauter, Aart Middeldorp and Harald Zankl Monotonicity Criteria for Polynomial Interpretations over the Naturals |
| 16:30 | Sarah Winkler and Aart Middeldorp Termination Tools in Ordered Completion |
| 17:00 | Albert Rubio Results of the Termination 2010 System Competition |
17:30‑18:00 Herbrand Award Ceremony
Location: AT LT5
| 17:30 | Maria Paola Bonacina (Master of Ceremony) Presentation of the Herbrand Award to David Plaisted |