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