Program of IJCAR

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
17:10‑17:50 Business Meeting
Location: AT LT5
17:10 IJCAR Business Meeting
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