Automated Reasoning

Session 1: Invited Talk.- Software Verification: Roles and Challenges for Automatic Decision Procedures.- Session 2: Specific Theories.- Proving Bounds on Real-Valued Functions with Computations.- Linear Quantifier Elimination.- Quantitative Separation Logic and Programs with Lists.- On Automating the Calculus of Relations.- Session 3: Automated Verification.- Towards SMT Model Checking of Array-Based Systems.- Preservation of Proof Obligations from Java to the Java Virtual Machine.- Efficient Well-Definedness Checking.- Session 4: Protocol Verification.- Proving Group Protocols Secure Against Eavesdroppers.- Session 5: System Descriptions 1.- Automated Implicit Computational Complexity Analysis (System Description).- LogAnswer - A Deduction-Based Question Answering System (System Description).- A High-Level Implementation of a System for Automated Reasoning with Default Rules (System Description).- The Abella Interactive Theorem Prover (System Description).- LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description).- KeYmaera: A Hybrid Theorem Prover for Hybrid Systems (System Description).- The Complexity of Conjunctive Query Answering in Expressive Description Logics.- A General Tableau Method for Deciding Description Logics, Modal Logics and Related First-Order Fragments.- Terminating Tableaux for Hybrid Logic with the Difference Modality and Converse.- Session 8: Herbrand Award Ceremony.- Automata-Based Axiom Pinpointing.- Individual Reuse in Description Logic Reasoning.- The Logical Difference Problem for Description Logic Terminologies.- Session 10: System Descriptions 2.- Aligator: A Mathematica Package for Invariant Generation (System Description).- leanCoP 2.0 and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions).- iProver - An Instantiation-Based Theorem Prover for First-Order Logic (System Description).- An Experimental Evaluation of Global Caching