20th International Conference on
Computer Aided Verification (CAV) 2008
July 7 – 14, 2008
Princeton, USA

CAV 2008 Overall Schedule

For Workshop schedules please check individual workshops.

 

CAV Conference Schedule

July 9
(Wednesday)		 Tutorials Day
8:45 — 9:00Opening Remarks
9:00 — 10:30Tutorial 1: Harry Foster, Mentor Graphics
Assertion-based Verification
10:30 — 11:00Break I
11:00 — 12:30Tutorial 2: John Harrison, Intel
Theorem Proving for Verification
12:30 — 2:00Lunch
2:00 — 3:30Tutorial 3: Peter O' Hearn, University of London
Tutorial on Separation Logic
3:30 — 4:00Break II
4:00 — 5:30Tutorial 4: Reinhard Wilhelm, Saarland University
Abstract Interpretation with Applications to Timing Validation
6:00 — 7:30Conference Reception
 
July 10
(Thursday) 		Conference
8:45 — 9:00Opening Remarks
9:00 — 10:00Invited Talk: Jim Larus, Microsoft Research
Singularity: Designing Better Software
10:00 — 10:30 Break I
10:30 — 12:30Session 1: Concurrency
10:30 — 11:00

Akash Lal and Thomas Reps
Reducing Concurrent Analysis Under a Context Bound to Sequential Analysis

11:00 — 11:30

Azadeh Farzan and Madhusudan Parthasarathy
Monitoring Atomicity in Concurrent Programs

11:30 — 12:00

Sarvani Vakkalanka, Ganesh Gopalakrishnan and Robert Kirby
Dynamic Verification of MPI programs with Reductions in Presence of Split Operations and Relaxed Orderings

12:00 — 12:30

Naoki Kobayashi and Davide Sangiorgi
A Hybrid Type System for Lock-Freedom of Mobile Processes

12:30 — 2:00 Lunch
2:00 — 3:30Session 2: Memory Consistency
2:00 — 2:30

Surender Baswana and Shashank Mehta
Implied Set Closure and Its Application to Memory Consistency Verification

2:30 — 3:00

Sebastian Burckhardt and Madanlal Musuvathi
Effective Program Verification for Relaxed Memory Models

3:00 — 3:30

Ariel Cohen, Amir Pnueli and Lenore Zuck
Mechanical Verification of Transactional Memories with Non-Transactional Memory Accesses

3:30 — 4:00 Break II
4:00 — 5:30Special Session: Ed Clarke, Allen Emerson, Joseph Sifakis
6:30 — 10:30Conference Banquet at Institute of Advanced Study, Princeton
 
July 11
(Friday)		 Conference
9:00 — 10:30Session 3: Decision Procedures
9:00 — 9:30

Himanshu Jain, Edmund Clarke and Orna Grumberg
Efficient Interpolation for Linear Diophantine (Dis)equations and Linear Modular Equations

9:30 — 10:00

Ruzica Piskac and Viktor Kuncak
Linear Arithmetic with Stars

10:00 — 10:30

Andy King and Harald Sondergaard
Inferring Congruence Equations with SAT

10:30 — 11:00 Break I
11:00 — 12:00 Session 4: Tools — Decision Procedures
11:00 — 11:15

Miquel Bofill, Robert Nieuwenhuis, Albert Oliveras, Enric Rodri­guez Carbonell and Albert Rubio.
The Barcelogic SMT solver

11:15 — 11:30

Roberto Bruttomesso, Alessandro Cimatti, Anders Franzen, Alberto Griggio and Roberto Sebastiani.
The MathSAT 4 SMT Solver

11:30 — 11:45

Dirk Beyer, Damien Zufferey and Rupak Majumdar
CSIsat: Interpolation for LA+EUF

11:45 — 12:00

Laura Meikle and Jacques Fleuriot
Prover's Palette: A User-Centric Approach to Verification with Isabelle and QEPCAD

12:00 — 12:15Hardware Model Checking Competition Report
12:30 — 2:00 Lunch
2:00 — 3:30 Session 5: Abstraction/Refinement
2:00 — 2:30

Mihaela Gheorghiu Bobaru, Corina Pasareanu and Dimitra Giannakopoulou
Automated Assume-Guarantee Reasoning by Abstraction Refinement

2:30 — 3:00

Ariel Cohen and Kedar Namjoshi
Local Proofs for Linear-Time Properties of Concurrent Programs

3:00 — 3:30

Holger Hermanns, Bjorn Wachter and Lijun Zhang
Probabilistic CEGAR

3:30 — 4:00 Break II
4:00 — 5:00Session 6: Hybrid Systems
4:00 — 4:30

Andre Platzer and Edmund Clarke
Computing Differential Invariants of Hybrid Systems as Fixedpoints

4:30 — 5:00

Sumit Gulwani and Ashish Tiwari
Constraint-based Approach for Analysis of Hybrid Systems

5:15 — 11:00 Manhattan Excursion (paid option)
 
July 12 (Saturday)Conference
9:00 — 10:00Invited Talk: Ed Felten, Princeton University
10:00 — 10:30 Break I
10:30 — 12:00Session 7: Modeling and Specification Formalisms
10:30 — 11:00

Salil Joshi and Barbara Konig
Applying the Graph Minor Theorem to the Verification of Graph Transformation Systems

11:00 — 11:30

Deepak D'Souza and Madhu Gopinathan
Conflict-Tolerant Features

11:30 — 12:00

Rajeev Alur, Aditya Kanade and Gera Weiss
Ranking Automata and Games for Prioritized Requirements

12:00 — 12:45Session 8: Tools — Security
12:00 — 12:15

Cas Cremers
The Scyther Tool: Verification, Falsification, and Analysis of Security Protocols

12:15 — 12:30

Michael Backes, Stefan Lorenz, Matteo Maffei and Kim Pecina
The CASPA Tool: Causality-based Abstraction for Security Protocol Analysis

12:30 — 12:45

Johannes Kinder and Helmut Veith
Jakstab: A Static Analysis Platform for Binaries

12:45 — 2:00 Lunch
2:00 — 4:00Session 9: Program Verification
2:00 — 2:30

Andreas Podelski, Andrey Rybalchenko and Thomas Wies
Heap Assumptions On Demand

2:30 — 3:00

Byron Cook, Sumit Gulwani, Tal Lev-Ami, Andrey Rybalchenko and Mooly Sagiv
Proving Conditional Termination

3:00 — 3:30

Parosh Abdulla, Ahmed Bouajjani, Jonathan Cederberg, Frederic Haziza and Ahmed Rezine.
Monotonic Abstraction for Programs with Dynamic Memory Heaps

3:30 — 4:00

Huu Hai Nguyen and Wei-Ngan Chin.
Enhancing Program Verification with Lemmas

4:00 — 4:30 Break II
4:30 — 6:15Session 10: Program and Shape Analysis
4:30 — 5:00

Bhargav Gulavani and Sumit Gulwani
A Numerical Abstract Domain based on "Expression Abstraction" and "Max Operator" with Application in Timing Analysis

5:00 — 5:30

Hongseok Yang, Oukseh Lee, Josh Berdine, Cristiano Calcagno, Byron Cook, Dino Distefano and Peter O'Hearn
Scalable Shape Analysis For Systems Code

5:30 — 6:00

Josh Berdine, Tal Lev-Ami, Roman Manevich, Ganesan Ramalingam and Mooly Sagiv
Thread Quantification for Concurrent Shape Analysis

6:00 — 6:15

Stephen Magill, Ming-Hsien Tsai, Peter Lee and Yih-Kuen Tsay.
THOR: A Tool for Reasoning about Shape and Arithmetic (Tool paper)

6:15 — 7:00CAV Business Meeting
 
July 13 (Sunday) Conference
9:00 — 10:00Session 11: Hardware Verification
9:00 — 9:30

Cindy Eisner, Amir Nahir and Karen Yorav
Functional Verification of Power Gated Designs by Compositional Reasoning

9:30 — 10:00

Per Bjesse
A Practical Approach to Word Level Model Checking of Industrial Netlists

10:00 — 10:30 Break I
10:30 — 11:30 (Session 11 Continued)
10:30 — 11:00

Sudipta Kundu, Sorin Lerner and Rajesh Gupta
Validating High Level Synthesis

11:00 — 11:30

Oliver Wienand, Markus Wedler, Dominik Stoffel, Wolfgang Kunz and Gert-Martin Greuel
An algebraic approach for proving data correctness in arithmetic data paths

11:30 — 12:15Session 12: Tools — Dynamic Verification
11:30 — 11:45

Ambar Gadkari, Anand Yeolekar, J Suresh, Ramesh S, Swarup Kumar Mohalik and K.C. Shashidhar
AutoMOTGen: Automatic Model Oriented Test Generator for Embedded Control Systems

11:45 — 12:00

Andreas Holzer, Christian Schallhart, Michael Tautschnig and Helmut Veith
FShell: Systematic Test Case Generation for Dynamic Analysis and Measurement

12:00 — 12:15

Kavita Ravi, Hyondeuk Kim, Hoonsang Jin, Petr Spacek, Robert P. Kurshan, Fabio Somenzi and John Pierce
Application of Formal Word-Level Analysis in Constrained Random Simulation

12:15 — 12:30 SMT-Comp Report
12:30 — 2:00 Lunch
2:00 — 3:00Session 13: Model Checking
2:00 — 2:30

Sujatha Kashyap and Vijay Garg
Producing short counterexamples using ``crucial events''

2:30 — 3:00

Peter Niebert, Doron Peled and Amir Pnueli
Discriminative Model Checking

3:00 — 4:00Session 14: Space Efficient Algorithms
3:00 — 3:30

Pavel Simecek, Stefan Edelkamp and Peter Sanders
Semi-External LTL Model Checking

3:30 — 4:00

Rob van Glabbeek and Bas Ploeger
Correcting a Space-Efficient Simulation Algorithm

4:00 — 4:30 Break II
4:30 — 5:15Session 15: Tools — Model Checking
4:30 — 4:45

Simon Gay, Rajagopal Nagarajan and Nikolaos Papanikolaou
QMC: A Model Checker for Quantum Systems

4:45 — 5:00

Axel Legay
T(O)RMC: A Tool for (Omega)-Regular Model Checking

5:00 — 5:15

Sebastian Kupferschmid, Martin Wehrle, Bernhard Nebel and Andreas Podelski
Faster than Uppaal?

End of Conference