The following boxes contain the daily schedule: talks etc. For a short overview of the schedule, see the schedule overview page. See this link for a single-page printable schedule without menus.

NB! Minor changes to the schedule and further details for social events are expected in the future.

8:30-9:00

Registration opens (it is OK to register later during the day, just make sure you do register sometimes before lunch).

9:00-10:00

DISPROVING workshop starts.

10:00-10:30

Coffee break.

10:30-12:45

DISPROVING workshop.

12:45-14:00

Lunch.

14:00-15:00

DISPROVING workshop finishes and ESCAR workshop starts with a shared invited talk.

15:00-16:00

ESCAR workshop.

16:00-16:30

Coffee break.

16:30-18:00

ESCAR workshop.

9:00-10:00

• ESCAR workshop second day.
• CFV'05 workshop starts.

10:00-10:30

Coffee break.

10:30-12:45

• ESCAR workshop second day.
• CFV'05 workshop.

12:45-14:00

Lunch.

14:00-16:00

• VERIFICATION OO tutorial.
• CFV'05 workshop.
• TPTP Tea Party.

16:00-16:30

Coffee break.

16:30-18:00

• VERIFICATION OO tutorial.
• CFV'05 workshop.
• TPTP Tea Party.

9:00-10:00

Invited talk by Gilles Dowek: What do we know when we know that a theory is consistent?

10:00-10:30

Coffee break.

10:30-12:30

• Evelyne Contejean and Pierre Corbineau.
  Reflecting Proofs in First-Order Logic with Equality
• Chad Brown.
  Reasoning in Extensional Type Theory with Equality
• Christian Urban and Christine Tasson.
  Nominal Techniques in Isabelle/HOL
• Brigitte Pientka.
  Tabling for higher-order logic programming

12:45-14:00

Lunch.

14:00-16:00

• Kaustuv Chaudhuri and Frank Pfenning.
  A Focusing Inverse Method Prover for First-Order Linear Logic
• Serge R. Autexier.
  The CORE Calculus
• Tal Lev-Ami, Neil Immerman, Siddharth Srivastava, Greta Yorsh, Mooly Sagiv and Thomas W. Reps.
  Simulating Reachability using First-Order Logic with Applications to Verification of Linked Data Structures
• Guillaume Dufay, Amy Felty and Stan Matwin.
  Privacy-Sensitive Information Flow with JML

16:00-16:30

Coffee break.

16:30-18:15

• Ting Zhang, Henny Sipma and Zohar Manna.
  The Decidability of the First-order theory of Knuth-Bendix Order
• Jordi Levy, Mateu Villaret and Joachim Niehren.
  Well-Nested Context Unification
• Guillem Godoy and Ashish Tiwari.
  Termination of Rewrite Systems with Shallow Right-Linear, Collapsing, and Right-Ground Rules
• Sean Bechhofer, Ian Horrocks and Daniele Turi.
  The OWL Instance Store (System Description)

Social events in the evening

• 19:00-20:30: Reception at the town hall.
• 20:30-21:30 Guided walking tour in the old town.
• CASQUE - the squash competition. Time and date subject to change.

9:00-10:00

Invited talk by Frank Wolter: Temporal logics over transitive states.

10:00-10:30

Coffee break.

10:30-12:15

• Ullrich Hustadt, Boris Konev and Renate A. Schmidt.
  Deciding monodic fragments by temporal resolution
• Viorica Sofronie-Stokkermans.
  Hierarchic reasoning in local theory extensions
• Claudio Castellini and Alan Smaill.
  Proof Planning for First-Order Temporal Logic
• Andreas Meier and Erica Melis.
  MULTI: A Multi-Strategy Proof Planner (System Description)

12:45-14:00

Lunch.

14:00-18:30

Excursion. Bus ride/walking/swimming at picturesque places, beaches and islands on the northern coast.

Social events in the evening (time TBA)

• CASC dinner.

09:00-10:00

Invited talk by Randal Bryant: Decision Procedures Customized for Formal Verification

10:00-10:30

• Coffee break.
• CASC starts.

10:30-12:15

• Viktor Kuncak, Hai, Huu Nguyen and Martin Rinard.
  An Algorithm for Deciding BAPA: Boolean Algebra with Presburger Arithmetic
• Franz Baader and Silvio Ghilardi.
  Connecting many-sorted theories
• John Harrison and Sean McLaughlin.
  A Proof Producing Decision Procedure for Real Arithmetic
• Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi Junttila, Peter van Rossum, Stephan Schulz and Roberto Sebastiani.
  MathSAT 3 (System Description)

12:45-14:00

Lunch.

14:00-16:00

• Tutorial by E. Giunchiglia: Beyond SAT: QSAT, and SAT-based Decision Procedures.
• Graham Steel.
  Deduction with XOR Constraints in Security API Modelling
• Kumar Neeraj Verma, Helmut Seidl and Thomas Schwentick.
  On the Complexity of Equational Horn Clauses

16:00-16:30

Coffee break.

16:30-17:15

• Greta Yorsh and Madan Musuvathi.
  A Combination Method for Generating Interpolants
• Marco Benedetti.
  sKizzo: A Suite to Evaluate and Certify QBFs (System Description)

17:30-19:00

• Herbrand award ceremony: Martin Davis.
• CADE business meeting.

Social events in the evening

• 19:15 Banquet at Olde Hansa.

9:00-10:00

Tutorial by Bruno Blanchet: An Automatic Security Protocol Verifier based on Resolution Theorem Proving.

10:00-10:30

Coffee break.

10:30-12:15

• Tomasz Truderung.
  Regular Protocols and Attacks with Regular Knowledge
• Peter Baumgartner and Cesare Tinelli.
  ME-E -- The Model Evolution Calculus with Equality
• Christian Fermüller and Reinhard Pichler.
  Model Representation via Contexts and Implicit Generalizations
• CASC: presentation of results.

12:45-14:00

Lunch.

14:00-15:15

• Mizuhito Ogawa, Eiichi Horita and Satoshi Ono.
  Proving Properties of Incremental Merkel Trees
• Jian Zhang.
  Computer Search for Counterexamples to Wilkie's Identity
• Alex Sinner and Thomas Kleemann.
  KRHyper - In Your Pocket (System Description)