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:00 Opening Remarks
Aarti Gupta, Sharad Malik

Invited Tutorial Introductions
Alan Hu
 

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
5:30 — 7:30Conference Reception
 
 
July 10
(Thursday)
Conference
8:45 — 9:00Welcome to CAV 2008
Aarti Gupta and Sharad Malik
 
9:00 — 10:00Invited Talk
Chair: Aarti Gupta

James Larus, Microsoft Research
Singularity: Designing Better Software

10:00 — 10:30 Break I
10:30 — 12:30 Session 1: Concurrency
Chair: Ahmed Bouajjani
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
Chair: Ganesh Gopalakrishnan
2:00 — 2:30

Surender Baswana, Shashank Mehta and Vishal Powar
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: ACM 2007 Turing Award Winners
Chair: Amir Pnueli

Edmund M. Clarke
BMC: Before Model Checking

E. Allen Emerson
Model Checking: A Personal Perspective

Joseph Sifakis
The Quest for Correctness -- Beyond Verification
 

6:00 — 10:30Conference Banquet at Institute for Advanced Study, Princeton
 
 
July 11
(Friday)
Conference
9:00 — 10:30 Session 3: Abstraction/Refinement
Chair: Orna Grumberg
9:00 — 9:30

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

9:30 — 10:00

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

10:00 — 10:30

Holger Hermanns, Bjorn Wachter and Lijun Zhang
Probabilistic CEGAR

10:30 — 11:00 Break I
11:00 — 12:00Session 4: Hybrid Systems
Chair: Holger Hermanns
11:00 — 11:30

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

11:30 — 12:00

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

12:00 — 12:30Session 5: Tools — Dynamic Verification
Chair: Oded Maler
12:00 — 12:15

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

12:15 — 12:30

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

12:30 — 2:00 Lunch
2:00 — 3:30Session 6: Modeling and Specification Formalisms
Chair: Roderick Bloem
2:00 — 2:30

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

2:30 — 3:00

Deepak D'Souza and Madhu Gopinathan
Conflict-Tolerant Features

3:00 — 3:30

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

3:30 — 4:00 Break II
4:00 — 5:30Session 7: Decision Procedures
Chair: John Harrison
4:00 — 4:30

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

4:30 — 5:00

Ruzica Piskac and Viktor Kuncak
Linear Arithmetic with Stars

5:00 — 5:30

Andy King and Harald Sondergaard
Inferring Congruence Equations with SAT

5:30 — 6:30 Session 8: Tools — Decision Procedures
Chair: Clark Barrett
5:30 — 5:45

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

5:45 — 6:00

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

6:00 — 6:15

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

6:15 — 6:30

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

6:30 — 7:15 CAV Business Meeting
 
 
July 12 (Saturday)Conference
9:00 — 10:00Invited Talk
Chair: Sharad Malik

Edward Felten, Princeton University
Coping with Outside-the-Box Attacks

10:00 — 10:30 Break I
10:30 — 12:30Session 9: Program Verification
Chair: Ken McMillan
10:30 — 11:00

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

11:00 — 11:30

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

11:30 — 12:00

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

12:00 — 12:30

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

12:30 — 1:30 Lunch
1:30 — 3:00Session 10: Program and Shape Analysis
Chair: Kedar Namjoshi
1:30 — 2:00

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

2:00 — 2:30

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

2:30 — 3:00

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

3:00 — 3:30 Break II
3:30 — 4:30Session 11: Tools — Security and Program Analysis
Chair: Daniel Kroening
3:30 — 3:45

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

3:45 — 4:00

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

4:00 — 4:15

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

4:15 — 4:30

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

4:45 — 11:45 Manhattan Cruise Excursion (paid option)
 
 
July 13 (Sunday) Conference
9:00 — 10:00Session 12: Hardware Verification I
Chair: Fabio Somenzi
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:45 Session 13: Hardware Verification II
Chair: Karen Yorav
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 — 11:45

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

11:45 — 12:00

Armin Biere
Hardware Model Checking Competition Report

12:00 — 12:15

Clark Barrett
SMT-Comp Report

12:15 — 2:00Lunch
2:00 — 3:00Session 14: Model Checking
Chair: Steven German
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 15: Space Efficient Algorithms
Chair: Lenore Zuck
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 16: Tools — Model Checking
Chair: Armin Biere
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