Monday July 29th

All assigned slots
See also the by-session program

CADE+CAV Invited talk (Aud. 1)
09:00  Malik: The quest for efficient Boolean satisfiability solvers
ICLP #1: Introduction and Best Papers (Aud. 4)
09:15  Introduction and Prize Giving
09:30  Russo, Miller, Nuseibeh, and Kramer: An abductive approach for analysing event-based requirements specifications
CAV #9: SAT Based Methods I (Aud. 1)
10:00  Barrett, Dill, and Stump: Checking satisfiability of first-order formulas by incremental translation to SAT
CADE #9 (Aud. 3)
10:00  Borralleras, Lucas, and Rubio: Recursive path orderings can be context-sensitive
10:00  Schrijvers, de la Banda, and Demoen: Trailing analysis for HAL


CAV #10: SAT Based Methods II (Aud. 1)
11:00  McMillan: Applying SAT methods in unbounded symbolic model checking
CADE #10: Combination of Decision Procedures (Aud. 3)
11:00  Ganzinger: Shostak light
ICLP #2: Applications I (Aud. 4)
11:00  Barker: Access control for deductive databases by logic programming
11:30  Clarke, Gupta, Kukula, and Strichman: SAT based abstraction-refinement using ILP and machine learning techniques11:30  Ford and Shankar: Formal verification of a combination decision procedure11:30  Lau and Bossche: Logic programming for software engineering: A second chance
12:00  Bingham and Hu: Semi-formal bounded model checking12:00  Zarba: Combining multisets with integers12:00  Bockmayr and Courtois: Using hybrid concurrent constraint programming to model dynamic biological systems


CAV #11: Symbolic Model Checking II (Aud. 1)
14:00  Bozzano and Delzanno: Algorithmic verification of invalidation-based protocols
CADE #11: Logical frameworks (Aud. 3)
14:00  Paulson: The reflection theorem: A study in formalizing meta-theoretic reasoning
ICLP #3: Invited Tutorial (Aud. 4)
14:00  Warren: Tabled logic programming
14:30  Jacobi: Formal verification of complex out-of-order pipelines by combining model-checking and theorem-proving14:30  Stump and Dill: Faster proof checking in the Edinburgh Logical Framework
15:00  Chevalier and Vigneron: Automated unbounded verification of security protocols15:00  Brown: Solving for set variables in higher-order theorem proving


CAV #12: Tool Presentations I (Aud. 1)
16:00  Alur, McDougall, and Yang: Exploiting behavioral hierarchy for efficient model checking
CADE #12: Model checking (Aud. 3)
16:00  Kupferman, Sattler, and Vardi: The complexity of the graded -calculus
ICLP #4: Tabling and Deductive Databases (Aud. 4)
16:00  Charatonik, Mukhopadhyay, and Podelski: Constraint-based infinite model checking and tabulation for stratified CLP
16:15  BOZGA, GRAF, and MOUNIER: IF-2.0: A validation environment for component-based real-time systems
16:30  Armando et al.: The AVISS security protocols analysis tool16:30  de Moura, Rue, and Sorea: Lazy theorem proving for bounded model checking over infinite domains16:30  Pemmasani, Ramakrishnan, and Ramakrishnan: Efficient real-time model checking using tabled logic programming and constraints
16:45  Asarin, Pace, Schneider, and Yovine: SPeeDI - a verification tool for polygonal hybrid systems
17:00  Cimatti et al.: NuSMV2: an opensource tool for symbolic model checking

17:00-18:00: CADE CADE business meeting (Aud. 3)

17:00  Jamil and Dobbie: A model theoretic semantics for multi-level secure deductive databases
17:15  Asarin, Dang, and Maler: The d/dt tool for verification of hybrid systems

17:30-18:30: ICLP Poster session (Lobby)

CoLogNET meeting (Aud. 2)
17:45  Presentation of CoLogNET and awareness launching on EU enlargement

18:40-19:00: ICLP ICLP Bus leaving to City Hall (Main entrance)

19:00-21:00: CADE+CAV+ICLP+TABLEAUX City Hall reception (City Hall)