Schedule of Papers and Events

Sunday, 10th August
AM	T2: Galois tutorial	T3: SMT tutorial	WS3: CEDAR workshop	WS2: PAAR workshop
PM	T4: COALA tutorial	WS1: VERIFY workshop	WS3: CEDAR workshop	WS2: PAAR workshop
Monday, 11th August
AM	T1: Isabelle tutorial	WS1: VERIFY workshop	WS4: CFV workshop	WS2: PAAR workshop
PM	T1: Isabelle tutorial	WS1: VERIFY workshop	WS4: CFV workshop	WS2: PAAR workshop
PPM	Reception
Tuesday, 12th August
AAM	Conference opening
AM	Invited talk and Papers
PM	Papers
PPM	TABLEAUX business meeting			CASC dinner
Wesnesday, 13th August
AM	Invited talk and Papers and Herbrand Award			CASC
PM	Papers
PPM	IJCAR and CADE business meetings
PPM	CASQ-J4
Thursday, 14th August
AM	Invited talk and Papers			TPTP Tea Party
PM	Excursion
PPM	Banquet
Friday, 15th August
AM	Invited talk and Papers
PM	Papers

Sunday, 10th August
	T2: Galois	T3: SMT	WS3: CEDAR	WS2: PAAR
09:00‑10:00	Tutorial Joe Hurd	Tutorial Nikolaj Bjørner, Leonardo de Moura	PAAR/CEDAR Invited Talk Software Model Checking: new challenges and opportunities for Automated Reasoning Alessandro Armando
10:30‑12:30			PTIME Description Logics with Functional Constraints and their Extensions David Toman, Grant Weddell Explaining User Errors in Description Logic Knowledge Base Completion Baris Sertkaya On the satisfiability problem for a 3-level quantified syllogistic Domenico Cantone, Marianna Nicolosi Asmundo	Towards fully automated axiom extraction for finite-valued logics Joao Marcos, Dalmo Mendonca Presenting TSTP Proofs with Inference Web Tools Paulo Pinheiro da Silva, Geoff Sutcliffe, Cynthia Chang, Li Ding, Nick del Rio, Deborah McGuinness Integration of the TPTPWorld into SigmaKEE Steven Trac, Geoff Sutcliffe, Adam Pease
	T4: COALA	WS1: VERIFY	WS3: CEDAR	WS2: PAAR
14:00‑15:30	Tutorial Dirk Pattinson	Invited Talk Operating System Verification for Real Use Gernot Heiser	Invited Talk Temporal Description Logics - A Survey Carsten Lutz Exploring Model-Based Development for the Verification of Real-Time Java Code Niusha Hakimipour, Paul Strooper, Roger Duke	ESHOL Invited Talk Mechanized Reasoning for Continuous Problem Domains Rob Arthan ESHOL System Demonstrations ProofPower Rob Arthan, Isabelle Stefan Berghofer, IsaPlanner Lucas Dixon
16:00‑17:30		Compositional Proofs with Symbolic Execution Simon Bäumler, Florian Nafz, Michael Balser, Wolfgang Reif Specification Predicates with Explicit Dependency Information Richard Bubel, Reiner Hähnle, Peter H. Schmitt Discussion	Incremental Instance Generation in Local Reasoning Swen Jacobs Towards Combining Dense Linear Orders with Random Graphs Jiamou Liu, Ting Zhang Concluding Remarks The Organizers	ESHOL System Demonstrations Coq Guillaume Melquiond , Mizar Josef Urban, HOL Joe Hurd, Delphin Carsten Schürmann, Omega and LEO Christoph Benzmüller, Frank Theiss, TPS Mark Kaminski
Monday, 11th August
	T1: Isabelle	WS1: VERIFY	WS4: CFV	WS2: PAAR
09:00‑10:00	Tutorial Christian Urban	VERIFY/CFV Invited Talk Putting Flight Software Through the Paces with Testing, Model Checking, and Constraint-Solving Alex Groce		ESHOL Invited Talk Constraint Modelling: A Challenge for First Order Automated Reasoning John Slaney
10:30‑12:30		Invited Talk Verification of Bit-Vector Arithmetic Priyank Kalla Model Stack for the Pervasive Verification of a Microkernel-based Operating System Matthias Daum, Jan Dörrenbächer, Sebastian Bogan Modular-HED: A Canonical Decision Diagram for Modular Equivalence Verification of Polynomial Functions Masahiro Fujita et al.		Contextual Rewriting in SPASS Christoph Weidenbach, Patrick Wischnewski Bit Inference Nachum Dershowitz A Small Framework for Proof Checking Hans de Nivelle, Piotr Witkowski
	T1: Isabelle	WS1: VERIFY	WS4: CFV	WS2: PAAR
14:00‑15:30	Tutorial Christian Urban	Invited Talk Certificate Translation Gilles Barthe Satisfiability Modulo Bit-precise Theories for Program Exploration Nikolaj Bjørner, Leonardo de Moura, Nikolai Tillmann		Collaborative Programming: Applications of logic and automated reasoning Timothy Hinrichs Combining Theorem Proving with Natural Language Processing Björn Pelzer and Ingo Glöckner
16:00‑18:00		Model Checking for Stability Analysis in Rely-Guarantee Proofs Hasan Amjad, Richard Bornat Bitfields and Tagged Unions in C: Verification through Automatic Generation David Cock Precise Dynamic Verification of Confidentiality Gurvan Le Guernic	Polynomial Function Enclosures and Floating Point Software Verification Jan Andrzej Duracz, Michal Konečný Quantitative Analysis of the SAT-Controlled Redundancy Addition and Removal Technique Chung-Yang (Ric) Huang and Chi-An Wu Adding Unsafe Constraints to Improve SAT Solver Performance John Franco, Sean Weaver Large Scale Genetic Identity Inference Using Symbolic Model Checking Rodrigo Gomes, Carolina Cota, Mark Song, Sergio Campos	The Annual SUMO Reasoning Prizes at CASC Adam Pease, Geoff Sutcliffe, Nick Siegel, Steven Trac randoCoP: Randomizing the Proof Search Order in the Connection Calculus Thomas Raths, Jens Otten ESHOL Panel Evaluation of Systems for Higher Order Logic Rob Arthan, Lucas Dixon, Joe Hurd
Tuesday, 12th August
08:45‑09:00 Conference opening	Opening and welcoming address Peter Baumgartner (Conference chair), Aruna Seneviratne (NICTA Lab Director and Director of Education)
09:00‑10:00 Session 1: Invited Talk Session chair: Peter Baumgartner	Software Verification: Roles and Challenges for Automatic Decision Procedures Aarti Gupta
10:30‑12:30 Session 2: Specific Theories Session chair: Franz Baader	Proving Bounds on Real-Valued Functions with Computations Guillaume Melquiond Linear Quantifier Elimination Tobias Nipkow Quantitative Separation Logic and Programs with Lists Radu Iosif, Marius Bozga, Swann Perarnau On Automating the Calculus of Relations Peter Höfner, Georg Struth
14:00‑15:30 Session 3: Automated Verification Session chair: Nikloj Bjørner	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
16:00‑16:30 Session 4: Protocol Verification Session chair: Alessandro Armando	Proving Group Protocols Secure Against Eavesdroppers Steve Kremer, Antoine Mercier, Ralf Treinen
16:30‑18:00 Session 5: System Descriptions 1 Session chair: Geoff Sutcliffe	Automated Implicit Computational Complexity Analysis (System Description) Martin Avanzini, Georg Moser, Andreas Schnabl LogAnswer - A Deduction-Based Question Answering System (System Description) Ulrich Furbach, Ingo Glöckner, Hermann Helbig, Björn Pelzer A High-Level Implementation of a System for Automated Reasoning with Default Rules (System Description) Christoph Beierle, Gabriele Kern-Isberner, Nicole Koch The Abella Interactive Theorem Prover (System Description) Andrew Gacek LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description) Christoph Benzmüller, Lawrence Paulson, Frank Theiss, Arnaud Fietzke KeYmaera: A Hybrid Theorem Prover for Hybrid Systems (System Description) Andre Platzer, Jan-David Quesel
19:00‑20:00 Business meeting	TABLEAUX business meeting Rajeev Goré (president)
Wednesday, 13th August
09:00‑10:00 Session 6: Invited Talk Session chair: Gilles Dowek	The Complexity of Conjunctive Query Answering in Expressive Description Logics Carsten Lutz
10:30‑11:30 Session 7: Modal Logics Session chair: Rajeev Goré	A General Tableau Method for Deciding Description Logics, Modal Logics and Related First-Order Fragments Renate Schmidt, Dmitry Tishkovsky Terminating Tableaux for Hybrid Logic with the Difference Modality and Converse Mark Kaminski, Gert Smolka
11:30‑12:15 Session 8: Herbrand Award Ceremony	Presentation of the Herbrand Award to Edmund Clarke Franz Baader (Master of Ceremony)
14:00‑15:30 Session 9: Description Logics Session chair: Renate Schmidt	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
16:00‑17:45 Session 10: System Descriptions 2 Session chair: Christoph Benzmüller	Aligator: A Mathematica Package for Invariant Generation (System Description) Laura Kovacs leanCoP 2.0 and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions) Jens Otten iProver - An instantiation-based theorem prover for first-order logic (System Description) Konstantin Korovin An Experimental Evaluation of Global Caching for ALC (System Description) Rajeev Gore, Linda Postniece Multi-Completion with Termination Tools (System Description) Haruhiko Sato, Sarah Winkler, Masahito Kurihara, Aart Middeldorp MTT: The Maude Termination Tool (System Description) Francisco Duran, Salvador Lucas, Jose Meseguer CELF - A Logical Framework for Deductive and Concurrent Systems (System Description) Anders Schack-Nielsen, Carsten Schürmann
18:00‑20:00 Business meetings	IJCAR and CADE business meetings Franz Baader (president)
Thursday, 14th August
09:00‑10:00 Session 11: Invited Talk Session chair: Maria Paola Bonacina	Canonicity! Nachum Dershowitz
10:30‑12:30 Session 12: Equational Theories Session chair: Tobias Nipkow	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, Georg Moser Canonical Inference for Implicational Systems Maria Paola Bonacina, Nachum Dershowitz
Friday, 15th August
09:00‑10:00 Session 13: Invited Talk Session chair: Alessandro Armando	Challenges in the Automated Verification of Security Protocols Hubert Comon-Lundh
10:30‑12:00 Session 14: Theorem Proving 1 Session chair: Hans de Nivelle	Deciding Effectively Propositional Logic using DPLL and substitution sets Leonardo de Moura, Nikolaj Bjørner Proof Systems for Effectively Propositional Logic Juan Antonio Navarro Perez, Andrei Voronkov MaLARea SG1: Machine Learner for Automated Reasoning with Semantic Guidance Josef Urban, Geoff Sutcliffe, Petr Pudlak, Jiri Vyskocil
12:00‑12:30 Session 15: CASC-J4	Presentation of CASC Results Geoff Sutcliffe (moderator) and the winners of the CASC divisions
14:00‑15:30 Session 16: Theorem Proving 2 Session chair: Ulrich Furbach	Labelled Splitting Arnaud Fietzke, Christoph Weidenbach Engineering DPLL(T) + Saturation Leonardo de Moura, Nikolaj Bjørner THF0 - The Core TPTP Language for Classical Higher-Order Logic Christoph Benzmüller, Florian Rabe, Geoff Sutcliffe
16:00‑16:30 Session 17: Logical Frameworks Session chair: Hubert Comon-Lundh	Focusing in linear meta-logic Vivek Nigam, Dale Miller
16:30‑17:30 Session 18: Tree Automata Session chair: Hubert Comon-Lundh	Certifying a Tree Automata Completion Checker Benoit Boyer, Thomas Genet, Thomas Jensen Automated Induction with Constrained Tree Automata Adel bouhoula, Florent Jacquemard