The CAV'05 conference and all co-located events take place July 6-12th, 2005.
All events take place at Appleton Tower Lecture Theatres, U. of Edinburgh.
The main CAV'05 conference days are July 7-10th.
On July 7-10th, lunches for CAV'05 participants will be served at Teviot House,
a short walk from Appleton Tower.
The CAV'05 tutorial day is July 6th.
6 affiliated workshops take place July 11-12th, with 3 on each day (see below).
(No lunches will be served on July 6th nor on July 11-12th.)

Tutorial Day: Wednesday, July 6, 2005.
(Appleton Tower, Lecture Theatre 2.)
(Chair of sessions: Sriram Rajamani)

• 9:00am-10:30am: Automated Abstraction Refinement I.
  By Thomas Ball and Ken McMillan.
  (Tom Ball's Tutorial Slides.)
• 10:30am-11:00am Coffee Break.

• 11:00am-12:30pm Automated Abstraction Refinement II.
  By Thomas Ball and Ken McMillan.

• 12:30pm-2:00pm Lunch

• 2:00pm-3:30pm Theory and Practice of Decision Procedures for Combinations of Theories, I.
  By Clark Barrett and Cesare Tinelli
  (Slides for Cesare Tinelli's tutorial.)

• 3:30pm-4:00pm Coffee Break

• 4:00pm-5:30pm Theory and Practice of Decision Procedures for Combinations of Theories, II.
  By Clark Barrett and Cesare Tinelli.
  (Clark Barett's Tutorial Slides.)

• 5:30pm - 7:00pm: Welcome Reception.

Day 1 of main conference: Thursday, July 7th.
(Appleton Tower, Lecture Theatre 4.)

• 8:45am Introduction and Welcome.

• 9:00am-10:00am Invited speaker: George Necula (U. C. Berkeley).
  Randomized Algorithms for Program Analysis and Verification.
  (Session Chair: Thomas Ball)

• 10:00am-10:30am Coffee Break.

• 10:30am -12:30pm Abstraction & Refinement
  (Session Chair: Kedar Namjoshi)
  • Predicate Abstraction via Symbolic Decision Procedures.
    Authors: Shuvendu Lahiri, Thomas Ball, Byron Cook

  • Interpolant-based Transition Relation Approximation.
      Authors: Kenneth McMillan, Ranjit Jhala

  • Concrete Model Checking with Abstract Matching and Refinement.
    Authors: Corina Pasareanu, Radek Pelánek, Willem Visser

  • Abstraction for Falsification.
    Authors: Thomas Ball, Orna Kupferman, Greta Yorsh

• 12:30pm-2:00pm Lunch.

• 2:00-4:00pm Bounded Model checking
  (Session Chair: Ken McMillan)
  • Bounded Model Checking of Concurrent Programs.
    Authors: Ishai Rabinovitz, Orna Grumberg

  • Incremental and Complete Bounded Model Checking for Full PLTL.
    Authors: Keijo Heljanko, Tommi Junttila, Timo Latvala

  • Abstraction Refinement for Bounded Model Checking.
    Authors: Anubhav Gupta, Ofer Strichman

  • Symmetry Reduction in SAT-based Model Checking.
    Authors: Daijue Tang, Sharad Malik, Aarti Gupta, C. Norris Ip

• 4:00pm-4:30pm Coffee Break.

• 4:30pm-6:00pm Tool session I.
  (Session Chair: Daniel Kroening)
  • Saturn: A SAT-based Tool for Bug Detection.
    Authors: Yichen Xie, Alex Aiken

  • JVer: a Java Verifier.
    Authors: Ajay Chander, David Espinosa, Nayeem Islam, Peter Lee, George Necula

  • Building Your Own Software Model Checker Using The BOGOR Extensible Model Checking Framework.
    Authors: Matthew Dwyer, John Hatcliff, Matthew Hoosier, Robby

  • Wolf - Bug Hunter for Concurrent Software using Formal Methods.
    Authors: Sharon Barner, Ziv Glazberg, Ishai Rabinovitz

  • Model Checking x86 Executables with CodeSurfer/x86 and WPDS++.
    Authors: Gogul Balakrishnan, Thomas Reps, Nick Kidd, Akash Lal, Junghee Lim, David Melski, Radu Gruian, Suan Yong, Chi-Hua Chen, Tim Teitelbaum

  • The ComFoRT Reasoning Framework.
    Authors: Sagar Chaki, James Ivers, Natalia Sharygina, Kurt Wallnau.

Day 2 of main conference. Friday, July 8th.
(Appleton Tower, Lecture Theatre 4.)

• 9:00am-10:00am Invited speaker: Bob Bentley (Intel Corp.).
  Validating a Modern Microprocessor (talk slides).
  (Session Chair: Bob Kurshan)

• 10:00am-10:30am Coffee Break.

• 10:30am -12:30pm Verification of hardware, microcode, & Synchronous systems
  (Session Chair: John O'Leary)
  • Formal Verification of Pentium 4 Components with Symbolic Simulation and Inductive Invariants.
    Authors: Roope Kaivola

  • Formal Verification of Backward Compatibility of Microcode.
    Authors: Tamarah Arons, Elad Elster, Limor Fix, Sela Mador-Haim, Michael Mishaeli, Jonathan Shalev, Eli Singerman, Andreas Tiemeyer, Moshe Vardi, Lenore Zuck

  • Compositional analysis of floating-point linear numerical filters.
    Authors: David Monniaux

  • Syntax-Driven Reachable State Space Construction of Synchronous Reactive Programs.
    Authors: Eric Vecchié, Robert de Simone

• 12:30pm-2:00pm Lunch.

• 2:00-4:00pm Games, and Probabilistic Verification
  (Session Chair: Ofer Strichman)
  • Program Repair as a Game.
    Authors: Barbara Jobstmann, Andreas Griesmayer, Roderick Bloem

  • Improved Probabilistic Models for 802.11 Protocol Verification.
    Authors: Amitabha Roy, K. Gopinath

  • Probabilistic Verification for ``Black-Box'' Systems.
    Authors: Håkan Younes

  • On Statistical Model Checking of Stochastic Systems.
    Authors: Koushik Sen, Mahesh Viswanathan, Gul Agha

• 4:00pm-4:30pm Coffee Break.

• 4:30pm-5:45pm Tool session II.
  (Session Chair: John Hatcliff)
  • The AVISPA Tool for the Automated Validation of Internet Security Protocols and Applications.
    Authors: Alessandro Armando, David Basin, Yohan Boichut, Yannick Chevalier, Luca Compagna, Jorge Cuellar, Paul Hankes Drielsma, Pierre-Cyrille Heám, Jacopo Mantovani, Sebastian Moedersheim, David von Oheimb, Michaël Rusinowitch, Judson Santiago, Mathieu Turuani, Luca Viganò, Laurent Vigneron

  • The Orchids Intrusion Detection Tool.
    Authors: Julien Olivain, Jean Goubault-Larrecq

  • TVOC: A Translation Validator for Optimizing Compilers.
    Authors: Clark Barrett, Yi Fang, Ben Goldberg, Ying Hu, Amir Pnueli, Lenore Zuck

  • Cogent: Accurate theorem proving for program verification.
    Authors: Byron Cook, Daniel Kroening, Natalia Sharygina

  • F-Soft: Software Verification Platform.
    Authors: Franjo Ivancic, Zijiang Yang, Malay K. Ganai, Aarti Gupta, Ilya Shlyakhter, Pranav Ashar

• 7:00-10:00pm CAV'05 Banquet (Dynamic Earth). In honor of Prof. Ed Clarke's 60th birthday.

Day 3 of main conference. Saturday, July 9th.
(Appleton Tower, Lecture Theatre 4.)

• 9:00am-10:00am Invited speaker: Bud Mishra (N.Y.U.).
  What's Next? Challenges from Systems Biology.
  (Session Chair: Ed Clarke)

• 10:00am-10:30am Coffee Break.

• 10:30am -12:00pm Decision procedures and applications
  (Session Chair: Sharad Malik)
  • Yet another Decision Procedure for Equality Logic.
    Authors: Orly Meir, Ofer Strichman

  • DPLL(T) with Exhaustive Theory Propagation and its Application to Difference Logic.
    Authors: Robert Nieuwenhuis, Albert Oliveras

  • Efficient Satisfiability Modulo Theories via Delayed Theory Combination.
    Authors: Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi Junttila, Silvio Ranise, Roberto Sebastiani, Peter van Rossum

• 12:00pm-2:00pm Lunch.

• 2:00-4:00pm Automata and transition systems
  (Session Chair: Orna Grumberg)
  • Symbolic Systems, Explicit Properties: on Hybrid Approaches for LTL Symbolic Model Checking.
    Authors: Roberto Sebastiani, Stefano Tonetta, Moshe Vardi

  • Efficient Monitoring of Omega-Languages.
    Authors: Marcelo d'Amorim, Grigore Rosu

  • Verification of Tree Updates for Optimization.
    Authors: Michael Benedikt, Angela Bonifati, Sergio Flesca, Avinash Vyas

  • Expand, Enlarge and Check... Made efficient.
    Authors: Gilles Geeraerts, Jean-François Raskin, Laurent Van Begin

• 4:00pm-4:30pm Coffee Break.

• 4:30pm-6:00pm Tool session III.
  (Session Chair: Helmut Veith)
  • Results of the Satisfiability Modulo Theories tool Competition. (co-located with CAV'05)
    Organizers: Clark Barrett, Leonardo Demoura, Aaron Stump

  • IIV: An Invisible Invariant Verifier.
    Authors: Ittai Balaban, Yi Fang, Amir Pnueli, Lenore Zuck

  • Action Language Verifier, Extended.
    Authors: Tuba Yavuz-Kahveci, Constantinos Bartzis, Tevfik Bultan

  • Romeo: A Tool for Analyzing Time Petri Nets.
    Authors: Guillaume Gardey, Didier Lime, Morgan Magnin, Olivier Roux

  • TRANSYT: a tool for the verification of asynchronous concurrent systems.
    Authors: Enric Pastor, Marco A. Peña, Marc Solé

  • Ymer: A Statistical Model Checker.
    Authors: Håkan Younes

• 6:15pm-7:15pm CAV'05 Business Meeting.

Day 4 of main conference. Sunday, July 10th.
(Appleton Tower, Lecture Theatre 4.)

• 9:00am-10:30am Program Analysis and Verification I
  (Session Chair: John Hatcliff)
  • Extended Weighted Pushdown Systems.
    Authors: Akash Lal, Thomas Reps, Gogul Balakrishnan

  • Incremental Algorithms for Inter-procedural Automaton-based Program Analysis.
    Authors: Christopher Conway, Dennis Dams, Stephen A. Edwards, Kedar Namjoshi

  • A policy iteration algorithm for computing fixed points in static analysis of programs.
    Authors: Alexandru Costan, Stéphane Gaubert, Eric Goubault, Matthieu Martel, Sylvie Putot

• 10:30am -11:00am Coffee Break.

• 11:00am -12:30pm Program Analysis and Verification II
  (Session Chair: P. Madhusudan)
  • Data Structure Specifications via Local Equality Axioms.
    Authors: Scott McPeak, George C. Necula

  • Linear Ranking with Reachability.
    Authors: Aaron Bradley, Zohar Manna, Henny Sipma

  • Reasoning about Threads Communicating via Locks.
    Authors: Vineet Kahlon, Franjo Ivancic, Aarti Gupta

• 12:30pm-2:00pm Lunch.

• 2:00pm-3:30pm Applications of Learning
  (Session Chair: Rupak Majumdar)
  • Abstraction Refinement via Inductive Learning.
    Authors: Alexey Loginov, Thomas Reps, Mooly Sagiv

  • Automated Assume-Guarantee Reasoning for Simulation Conformance.
    Authors: Sagar Chaki, Edmund Clarke, Nishant Sinha, Prasanna Thati

  • Symbolic Compositional Verification by Learning Assumptions.
    Authors: Rajeev Alur, P. Madhusudan, Wonhong Nam

• END OF MAIN CAV'05 CONFERENCE

Co-located Events (July 6-12):

• "Satisfiability Modulo Theories Competition" (July 6-10): a special tools competition. (Appleton Tower, 5th floor computer lab.)

Workshop Day 1, Monday, July 11th.
(Appleton Tower Lecture Theatres, 8:45am-6:30pm.)

• BMC'2005: 3rd Int. Workshop on Bounded Model Checking.
  (Appleton Tower, Lecture Theatre 1.)
  Organizers: Armin Biere and Ofer Strichman.

• FATES'2005: 5th Workshop on Formal Approaches to Testing Software.
  (Appleton Tower, Lecture Theatre 2.)
  Organizers: W. Grieskamp and C. Weise.

• SoftMC'2005: 3rd Workshop on Software Model Checking.
  (Appleton Tower, Lecture Theatre 3.)
  Organizers: Byron Cook, Scott Stoller, and Willem Visser.

Workshop Day 2, Tuesday, July 12th.
(Appleton Tower Lecture Theatres, 8:45am-6:30pm.)

• GDV'2005 (July 12): 2nd Workshop on Games in Design and Verification.
  (Appleton Tower, Lecture Theatre 1.)
  Organizers: M. Jurdzinski and R. Majumdar.

• PDPAR'2005 (July 12): 3rd Workshop on Pragmatics of Decision Procedures in Automated Reasoning.
  (Appleton Tower, Lecture Theatre 2.)
  Organizers: Alessandro Armando and Alessandro Cimatti.

• RV'2005 (July 12): 5th Workshop on Runtime verification.
  (Appleton Tower, Lecture Theatre 3.)
  Organizers: H. Barringer, B. Finkbeiner, Y. Gurevich,and H. Sipma.