Saturday July 27th

All assigned slots
See also the by-session program

PCL #1: Axioms (Aud. 7)
08:55  Opening and Welcome
CAV #1: Tutorial I (Aud. 1)
Invited tutorial
09:00  Thomas: Infinite games and verification
CADE #1: Description logics and Semantic Web (Aud. 3)
Invited talk
09:00  Horrocks: Reasoning with expressive description logics: Theory and practice
09:00  Besnard, Schaub, Tompits, and Woltran: Paraconsistent reasoning via quantified boolean formulas, I: Axiomatising signed systemsSAVE #1 (Aud. 8)
Invited talk
09:00  Katoen: Model checking birth and death
09:30  Zhang: Axiomatic aspects of default inference
09:45  Sharygina and Browne: Model checking large-scale software via abstraction of loop transitions
10:00  Coffee Break10:00  Pan, Sattler, and Vardi: BDD-based decision procedures for K10:00  Villadsen: A paraconsistent higher order logic
10:15  Thomas continued


CADE #2: Proof-carrying code and compiler verification (Aud. 3)
11:00  Bernard and Lee: Temporal logic for proof-carrying code
PCL #2: Models and Sets (Aud. 7)
11:00  Arieli, Denecker, Nuffelen, and Bruynooghe: Repairing inconsistent databases: A model-theoretic approach and abductive reasoning
SAVE #2 (Aud. 8)
11:00  Armando and Lucia: Symbolic model-checking of linear programs
CAV #2: Tutorial IIa (Aud. 1)
Invited tutorial
11:30  Cousot: On abstraction in software verification
11:30  Necula and Schneck: A gradual approach to a more trustworthy, yet scalable, proof-carrying code11:30  Maher: A model-theoretic semantics for defeasible logic
11:45  Ammirati, Delzanno, Ganty, Geeraerts, Raskin, and Begin: Babylon: An integrated toolkit for the specification and verification of parameterized systems
12:00  Strecker: Formal verification of a java compiler in isabelle12:00  Maluszynski and Vitória: Defining rough sets by extended logic programs


PCL #3: Dynamics, Interaction and Nonmonotonicity (Aud. 7)
Invited talk
13:45  Batens: On a partial decision method for dynamic proofs
CAV #3: Tutorial IIb (Aud. 1)
14:00  Cousot continued
CADE #3: Non-classical logics (Aud. 3)
14:00  Egly: Embedding lax logic into intuitionistic logic
SAVE #3 (Aud. 8)
Invited talk
14:00  Armando: An overview of the AVISS project
14:30  Larchey-Wendling: Combining proof-search and counter-model construction for deciding Gödel-Dummett logic14:30  Goldin and Wegner: Paraconsistency of interactive computation
14:45  Aziz and Hamilton: A privacy analysis for the π-calculus: The denotational approach
15:00  Galmiche and Mery: Connection-based proof search in propositional BI logic15:00  Bry: An almost classical logic for logic programming and nonmonotonic reasoning
CAV #4: Tutorial III (Aud. 1)
Invited tutorial
15:15  Henzinger: The symbolic approach to hybrid systems


CADE #4: System descriptions (Aud. 3)
16:00  Mřller: DDDLIB: A library for solving quantified difference inequalities
PCL #4: Panel and Other Issues (Aud. 7)
16:00  Panel: Paraconsistency and Logic Programming -- An Odd Couple or a Natural Pairing?
SAVE #4 (Aud. 8)
16:00  Martinelli: Symbolic partial model checking for security analysis
16:15  Coffee Break16:15  Hurd: An LCF-style interface between HOL and first-order logic
16:30  Henzinger continued16:30  Kohlhase and Zimmer: System description: The MathWeb software bus for distributed mathmatical reasoning
16:45  Siekmann et al.: Proof development with OMEGA16:45  Discussion: Publication of Proceedings16:45  Corin and Etalle: An improved constraint-based system for the verification of security protocols
17:00  Jamnik, Kerber, and Pollet: LearnOmatic: System description
17:15  Areces and Heguiabehere: HyLoRes 1.0: Direct resolution for hybrid logics17:15  Closing

17:30-19:00: CADE+CAV Welcome reception (Lobby)

19:00-21:00: PCL Dinner (Restaurant A Hereford Beefstouw)

19:30-21:00: CADE CASC dinner (Restaurant Da Mario)