Monday 16. November, 1st Conference Day

08:15 - 08:45 Registration

08:45 - 09:00 Opening (chairs Armin Biere, Carl Pixley)

09:00 - 10:30 Session 1 (chair Gianpiero Cabodi)

Model Checking

   Yakir Vizel and Orna Grumberg.
   Interpolation-Sequence Based Model Checking.

   Alessandro Cimatti, Jori Dubrovin, Tommi Junttila and Marco Roveri.
   Structure-Aware Computation of Predicate Abstraction.

   Michael Case, Hari Mony, Jason Baumgartner and Robert Kanzelman.
   Enhanced Verification by Temporal Decomposition.

10:30 - 11:00 Coffee

11:00 - 12:20 Session 2 (chair Daniel Kroening)

Software Verification

   Dirk Beyer, Alessandro Cimatti, Alberto Griggio,
   M. Erkan Keremoglu and Roberto Sebastiani.
   Software Model Checking via Large-Block Encoding.

   Jyotirmoy Deshmukh and E. Allen Emerson.
   Verification of Recursive Methods on Tree-like Data Structures.

   Subodh Sharma, Ganesh Gopalakrishnan, Eric Mercer and Jim Holt.
   MCC - A runtime verification tool for MCAPI user applications
   (short paper).

12:20 - 12:30 In Memoriam: Amir Pnueli (chair Moshe Vardi)

12:30 - 14:00 Lunch

14:00 - 15:00 Keynote (chair Armin Biere)

  E. Allen Emerson, University of Texas at Austin.

15:00 - 15:30 Coffee

15:30 - 17:30 Session 3 (chair Cesare Tinelli)

Satisfiability Modulo Theory 

   Leonardo de Moura and Nikolaj Bjorner.
   Generalized and Efficient Array Decision Procedures.

   Sagar Chaki, Arie Gurfinkel and Ofer Strichman.
   Decision Diagrams for Linear Arithmetic.

   Malay Ganai and Franjo Ivancic.
   Efficient Decision Procedure for Non-linear Arithmetic Constraints
   using CORDIC.

   Angelo Brillout, Daniel Kroening and Thomas Wahl.
   Mixed Abstractions for Floating-Point Arithmetic.

18:00 - 19:00 Business Meeting (chair Warren Hunt)