Invited Talk / Session 1: |
Software Verification: Roles and Challenges for Automatic Decision Procedures / Aarti Gupta |
Specific Theories / Session 2: |
Proving Bounds on Real-Valued Functions with Computations / Guillaume Melquiond |
Linear Quantifier Elimination / Tobias Nipkow |
Quantitative Separation Logic and Programs with Lists / Marius Bozga ; Radu Iosif ; Swann Perarnau |
On Automating the Calculus of Relations / Peter Hofner ; Georg Struth |
Automated Verification / Session 3: |
Towards SMT Model Checking of Array-Based Systems / Silvio Ghilardi ; Enrica Nicolini ; Silvio Ranise ; Daniele Zucchelli |
Preservation of Proof Obligations from Java to the Java Virtual Machine / Gilles Barthe ; Benjamin Gregoire ; Mariela Pavlova |
Efficient Well-Definedness Checking / Adam Darvas ; Farhad Mehta ; Arsenii Rudich |
Protocol Verification / Session 4: |
Proving Group Protocols Secure Against Eavesdroppers / Steve Kremer ; Antoine Mercier ; Ralf Treinen |
System Descriptions 1 / Session 5: |
Automated Implicit Computational Complexity Analysis / Martin Avanzini ; Georg Moser ; Andreas Schnabl |
LogAnswer - A Deduction-Based Question Answering System / Ulrich Furbach ; Ingo Glockner ; Hermann Helbig ; Bjorn Pelzer |
A High-Level Implementation of a System for Automated Reasoning with Default Rules / Christoph Beierle ; Gabriele Kern-Isberner ; Nicole Koch |
The Abella Interactive Theorem Prover / Andrew Gacek |
LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic / Christoph Benzmuller ; Lawrence C. Paulson ; Frank Theiss ; Arnaud Fietzke |
KeYmaera: A Hybrid Theorem Prover for Hybrid Systems / Andre Platzer ; Jan-David Quesel |
The Complexity of Conjunctive Query Answering in Expressive Description Logics / Carsten LutzSession 6: |
Modal Logics / Session 7: |
A General Tableau Method for Deciding Description Logics, Modal Logics and Related First-Order Fragments / Renate A. Schmidt ; Dmitry Tishkovsky |
Terminating Tableaux for Hybrid Logic with the Difference Modality and Converse / Mark Kaminski ; Gert Smolka |
Herbrand Award Ceremony / Session 8: |
Description Logics / Session 9: |
Automata-Based Axiom Pinpointing / Franz Baader ; Rafael Penaloza |
Individual Reuse in Description Logic Reasoning / Boris Motik ; Ian Horrocks |
The Logical Difference Problem for Description Logic Terminologies / Boris Konev ; Dirk Walther ; Frank Wolter |
System Descriptions 2 / Session 10: |
Aligator: A Mathematica Package for Invariant Generation / Laura Kovacs |
IeanCoP 2.0 and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic / Jens Otten |
iProver - An Instantiation-Based Theorem Prover for First-Order Logic / Konstantin Korovin |
An Experimental Evaluation of Global Caching for ALC / Rajeev Gore ; Linda Postniece |
Multi-completion with Termination Tools / Haruhiko Sato ; Sarah Winkler ; Masahito Kurihara ; Aart Middeldorp |
MTT: The Maude Termination Tool / Francisco Duran ; Salvador Lucas ; Jose Meseguer |
Celf - A Logical Framework for Deductive and Concurrent Systems / Anders Schack-Nielsen ; Carsten Schurmann |
Canonicity! / Nachum DershowitzSession 11: |
Equational Theories / Session 12: |
Unification and Matching Modulo Leaf-Permutative Equational Presentations / Thierry Boy de la Tour ; Mnacho Echenim ; Paliath Narendran |
Modularity of Confluence: Constructed / Vincent van Oostrom |
Automated Complexity Analysis Based on the Dependency Pair Method / Nao Hirokawa ; Geory Moser |
Canonical Inference for Implicational Systems / Maria Paola Bonacina |
Challenges in the Automated Verification of Security Protocols / Hubert Comon-LundhSession 13: |
Theorem Proving 1 / Session 14: |
Deciding Effectively Propositional Logic Using DPLL and Substitution Sets / Leonardo de Moura ; Nikolaj Bjorner |
Proof Systems for Effectively Propositional Logic / Juan Antonio Navarro ; Andrei Voronkov |
MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance / Josef Urban ; Geoff Sutcliffe ; Petr Pudlak ; Jiri Vyskocil |
CASC / Session 15: |
CASC-J4 - The 4th IJCAR ATP System Competition |
Theorem Proving 2 / Session 16: |
Labelled Splitting / Christoph Weidenbach |
Engineering DPLL(T) + Saturation |
THF0 - The Core of the TPTP Language for Higher-Order Logic / Florian Rabe |
Logical Frameworks / Session 17: |
Focusing in Linear Meta-logic / Vivek Nigam ; Dale Miller |
Tree Automata / Session 18: |
Certifying a Tree Automata Completion Checker / Benoit Boyer ; Thomas Genet ; Thomas Jensen |
Automated Induction with Constrained Tree Automata / Adel Bouhoula ; Florent Jacquemard |
Author Index |
Invited Talk / Session 1: |
Software Verification: Roles and Challenges for Automatic Decision Procedures / Aarti Gupta |
Specific Theories / Session 2: |