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