| CAV 2006 | Computer-Aided Verification Seattle, August 17 - 20, 2006 |
Program
Wednesday, August 16th
Wednesday's program is also available side by side with other meetings.
19:00‑21:00 CAV-ICLP-IJCAR Joint Reception
Location:
Grand Ballroom A/B
Thursday, August 17th
Thursday's program is also available with abstracts or side by side with other meetings.
08:45‑10:00 FLoC Second Opening and Plenary Session
Chair:
Moshe Vardi, Thomas Ball, Wolfram Schulte, Ken McMillan
Location:
Metropolitan A/B
| 08:45 | Introduction and Welcome |
| 09:00 | David Dill
(Stanford University) I Think I Voted: E-voting vs. Democracy [ppt] |
10:00‑10:30 Break
10:30‑12:00 Session 1: Automata
Chair:
Amir Pnueli
Location:
Metropolitan A
| 10:30 | Martin De Wulf, Laurent Doyen, Tom Henzinger and Jean-Francois Raskin
Antichains: A New Algorithm for Checking Universality of Finite Automata |
| 11:00 | Orna Kupferman
, Moshe Y. Vardi and Nir Piterman
Safraless Compositional Synthesis |
| 11:30 | Sudeep Juvekar
and Nir Piterman
Minimizing Generalized Buchi Automata |
12:00‑12:30 Session 2: Tools Papers
Chair:
Amir Pnuelo
Location:
Metropolitan A
| 12:00 | Luca de Alfaro
, Marco Faella, B. Thomas Adler, Leandro Dias Da Silva, Axel Legay, Vishwanath Raman
and Pritam Roy Ticc: A Tool for Interface Compatibility and Composition |
| 12:15 | Sébastien Bardin
, Jerome Leroux
and Gérald Point FAST Extended Release |
12:30‑14:00 Lunch break
14:00‑15:00 Session 3: Arithmetic
Chair:
Sanjit A. Seshia
Location:
Metropolitan A
15:00‑16:00 Session 4: SAT and Bounded Model Checking
Chair:
Clark Barrett
Location:
Metropolitan A
| 15:00 | Keijo Heljanko
, Tommi Junttila
, Misa Keinänen
, Martin Lange
and Timo Latvala
Bounded Model Checking for Weak Alternating Buchi Automata |
| 15:30 | Roman Gershman, Maya Koifman and Ofer Strichman
Deriving small unsatisfiable cores with dominators |
16:00‑16:30 Break
16:30‑17:30 Invited Talk
Chair:
Thomas Ball
Location:
Metropolitan A
| 16:30 | Manuvir Das
(Microsoft) Formal Specifications on Industrial-Strength Code - From Myth to Reality [ppt] |
Friday, August 18th
Friday's program is also available with abstracts or side by side with other meetings.
09:00‑10:00 Invited Talk
Chair:
Ed Clarke
Location:
Metropolitan A
| 09:00 | Tony Hoare
(Microsoft Research) The Ideal of Verified Software [ppt] |
10:00‑10:30 Break
10:30‑12:00 Session 5: Abstraction/Refinement
Chair:
Orna Grumberg
Location:
Metropolitan A
| 10:30 | Kenneth McMillan
Lazy Abstraction with Interpolants |
| 11:00 | Himanshu Jain
, Franjo Ivancic, Aarti Gupta, Ilya Shlyakhter
and Chao Wang
Using Statically Computed Invariants inside the Predicate Abstraction and Refinement Loop |
| 11:30 | Daniel Kroening
and Georg Weissenbacher Counterexamples with Loops for Predicate Abstraction |
12:00‑12:30 Session 6: Tools Papers
Chair:
Orna Grumberg
Location:
Metropolitan A
| 12:00 | Nikhil Sethi
and Clark Barrett
Cascade: C Assertion Checker and Deductive Engine |
| 12:15 | Arie Gurfinkel
, Ou Wei and marsha chechik
Yasm: A Software Model-Checker for Verification and Refutation |
12:30‑14:00 Lunch break
14:00‑15:00 Session 7: Symbolic Trajectory Evaluation
Chair:
Fabio Somenzi
Location:
Metropolitan A
15:00‑16:00 Session 8: Property Specification and Verification
Chair:
Fabio Somenzi
Location:
Metropolitan A
| 15:00 | Doron Bustan
and John Havlicek Some complexity results for SystemVerilog Assertions |
| 15:30 | Jochen Klose, Tobe Toben, Bernd Westphal and Hartmut Wittke Check It Out: On the Efficient Formal Verification of Live Sequence Charts |
16:00‑16:30 Break
16:30‑18:00 Session 9: Time
Chair:
Holger Hermanns
Location:
Metropolitan A
18:00‑18:30 Session 10: Tools Papers
Chair:
Holger Hermanns
Location:
Metropolitan A
| 18:00 | Jiri Barnat, Lubos Brim, Ivana Cerna, Pavel Moravec, Petr Rockai and Pavel Simecek DiVinE - A Tool for Distributed Verification |
| 18:15 | Flavio M. de Paula
and Alan Hu
EverLost: A Flexible Platform for Industrial-Strength Abstraction-Guided Simulation |
19:00‑22:30 CAV-IJCAR Joint Cruise/Banquet
Location:
depart Spirit of Seattle from Pier 55
| 19:00 |
CAV-IJCAR Joint Cruise/Banquet Boarding from Pier 55 (walking distance from hotel) |
| 19:30 | CAV-IJCAR Joint Cruise/Banquet |
Saturday, August 19th
Saturday's program is also available with abstracts or side by side with other meetings.
09:00‑10:30 Session 11: Concurrency
Chair:
Ahmed Bouajjani
Location:
Grand Ballroom C
| 09:00 | Vineet Kahlon, Aarti Gupta and Nishant Sinha
Symbolic Model Checking of Concurrent Programs using Partial Orders and On-the-fly Transactions |
| 09:30 | Koushik Sen
and Mahesh Viswanathan Model Checking Multithreaded Programs with Asynchronous Atomic Methods |
| 10:00 | Azadeh Farzan
and P. Madhusudan
Causal Atomicity |
10:30‑11:00 Break
11:00‑12:30 Session 12: Trees, Pushdown Systems and Boolean Programs
Chair:
Ranjit Jhala
Location:
Grand Ballroom C
12:30‑14:00 Lunch (in hotel)
Location:
Grand Ballroom D
14:00‑15:30 Session 13: Termination
Chair:
Thomas Ball
Location:
Grand Ballroom C
15:30‑16:00 Session 14: Tools Papers
Chair:
Thomas Ball
Location:
Grand Ballroom C
| 15:30 | Byron Cook
, Andreas Podelski and Andrey Rybalchenko
Terminator: Beyond Safety |
| 15:45 | Koushik Sen
and Gul Agha
CUTE and jCUTE : Concolic Unit Testing and Explicit Path Model-Checking Tools |
16:00‑16:30 Break
16:30‑17:30 Keynote Session
Chair:
Wolfram Schulte, Moshe Vardi
Location:
Grand Ballroom B/C
| 16:30 | David Harel
(Weizmann Institute) Playing with Verification, Planning and Aspects: Unusual Methods for Running Scenario-Based Programs [ppt] |
18:00‑19:00 CAV Business Meeting
Location:
Grand Ballroom C
Sunday, August 20th
Sunday's program is also available with abstracts or side by side with other meetings.
09:00‑10:00 Invited Talk
Chair:
Robert Jones
Location:
Grand Ballroom C
| 09:00 | Joe Stoy
(Bluespec) Verification? Getting it Right the First Time [ppt] |
10:00‑10:30 Break
10:30‑12:00 Session 15: Abstract Interpretation
Chair:
Robert Jones
Location:
Grand Ballroom C
| 10:30 | Shuvendu Lahiri
, Robert Nieuwenhuis
and Albert Oliveras
SMT Techniques for Predicate Abstraction |
| 11:00 | Bernard Boigelot
and Frédéric Herbreteau
The Power of Hybrid Acceleration |
| 11:30 | Denis Gopan and Thomas Reps
Lookahead Widening |
12:00‑12:30 Session 16: Tools Papers
Chair:
Robert Jones
Location:
Grand Ballroom C
| 12:00 | Kenneth Roe
The Heuristic Theorem Prover: Yet another SMT Modulo Theorem Prover |
| 12:15 | Abhay Vardhan and Mahesh Viswanathan LEVER: A tool for Learning Based Verification |
12:30‑14:00 Lunch break
14:00‑15:30 Session 17: Memory Consistency
Chair:
Ganesh Gopalakrishnan
Location:
Grand Ballroom C
| 14:00 | Robert Colvin, Lindsay Groves, Victor Luchangco and Mark Moir Formal Verification of a Lazy Concurrent List-Based Set |
| 14:30 | Sebastian Burckhardt
, Rajeev Alur
and Milo M.K. Martin
Bounded Model Checking of Concurrent Data Types on Relaxed Memory Models: A Case Study |
| 15:00 | Amitabha Roy, Chuck Fleckenstein, Stephan Zeisset and John Huang Fast and Generalized Polynomial Time Memory Consistency Verification |
15:30‑16:00 Break
16:00‑17:30 Session 18: Shape Analysis
Chair:
Thomas Ball
Location:
Grand Ballroom C
| 16:00 | Radu Iosif
, Marius Bozga, Ahmed Bouajjani, Peter Habermehl, Pierre Moro and Tomas Vojnar Programs with Lists are Counter Automata |
| 16:30 | Dirk Beyer
, Tom Henzinger and Grégory Théoduloz
Lazy Shape Analysis |
| 17:00 | Tal Lev-Ami
, Neil Immerman and Mooly Sagiv
Abstraction for Shape Analysis with Fast and Precise Transformers |
17:30‑17:45 SMT-COMP report
Chair:
Clark Barrett, Aaron Stump, Leonardo de Moura
Location:
Grand Ballroom C
