18. CAV 2006: Seattle, WA, USA

Thomas Ball, Robert B. Jones (Eds.): Computer Aided Verification, 18th International Conference, CAV 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings. Lecture Notes in Computer Science 4144 Springer 2006, ISBN 3-540-37406-X BibTeX

Invited Talks

Manuvir Das:
Formal Specifications on Industrial-Strength Code-From Myth to Reality. 1
Electronic Edition (link) BibTeX
David L. Dill:
I Think I Voted: E-Voting vs. Democracy. 2
Electronic Edition (link) BibTeX
David Harel:
Playing with Verification, Planning and Aspects: Unusual Methods for Running Scenario-Based Programs. 3-4
Electronic Edition (link) BibTeX
Tony Hoare:
The Ideal of Verified Software. 5-16
Electronic Edition (link) BibTeX

Martin De Wulf, Laurent Doyen, Thomas A. Henzinger, Jean-François Raskin:
Antichains: A New Algorithm for Checking Universality of Finite Automata. 17-30
Electronic Edition (link) BibTeX
Orna Kupferman, Nir Piterman, Moshe Y. Vardi:
Safraless Compositional Synthesis. 31-44
Electronic Edition (link) BibTeX
Sudeep Juvekar, Nir Piterman:
Minimizing Generalized Büchi Automata. 45-58
Electronic Edition (link) BibTeX

Jochen Eisinger, Felix Klaedtke:
Don't Care Words with an Application to the Automata-Based Approach for Real Addition. 67-80
Electronic Edition (link) BibTeX
Bruno Dutertre, Leonardo Mendonça de Moura:
A Fast Linear-Arithmetic Solver for DPLL(T). 81-94
Electronic Edition (link) BibTeX

Keijo Heljanko, Tommi A. Junttila, Misa Keinänen, Martin Lange, Timo Latvala:
Bounded Model Checking for Weak Alternating Büchi Automata. 95-108
Electronic Edition (link) BibTeX
Roman Gershman, Maya Koifman, Ofer Strichman:
Deriving Small Unsatisfiable Cores with Dominators. 109-122
Electronic Edition (link) BibTeX

Kenneth L. McMillan:
Lazy Abstraction with Interpolants. 123-136
Electronic Edition (link) BibTeX
Himanshu Jain, Franjo Ivancic, Aarti Gupta, Ilya Shlyakhter, Chao Wang:
Using Statically Computed Invariants Inside the Predicate Abstraction and Refinement Loop. 137-151
Electronic Edition (link) BibTeX
Daniel Kroening, Georg Weissenbacher:
Counterexamples with Loops for Predicate Abstraction. 152-165
Electronic Edition (link) BibTeX

Nikhil Sethi, Clark Barrett:
cascade: C Assertion Checker and Deductive Engine. 166-169
Electronic Edition (link) BibTeX
Arie Gurfinkel, Ou Wei, Marsha Chechik:
Yasm: A Software Model-Checker for Verification and Refutation. 170-174
Electronic Edition (link) BibTeX

Jan-Willem Roorda, Koen Claessen:
SAT-Based Assistance in Abstraction Refinement for Symbolic Trajectory Evaluation. 175-189
Electronic Edition (link) BibTeX
Rachel Tzoref, Orna Grumberg:
Automatic Refinement and Vacuity Detection for Symbolic Trajectory Evaluation. 190-204
Electronic Edition (link) BibTeX

Doron Bustan, John Havlicek:
Some Complexity Results for SystemVerilog Assertions. 205-218
Electronic Edition (link) BibTeX
Jochen Klose, Tobe Toben, Bernd Westphal, Hartmut Wittke:
Check It Out: On the Efficient Formal Verification of Live Sequence Charts. 219-233
Electronic Edition (link) BibTeX

Marta Z. Kwiatkowska, Gethin Norman, David Parker:
Symmetry Reduction for Probabilistic Model Checking. 234-248
Electronic Edition (link) BibTeX
Pavel Krcál, Wang Yi:
Communicating Timed Automata: The More Synchronous, the More Difficult to Verify. 249-262
Electronic Edition (link) BibTeX
Grigore Rosu, Saddek Bensalem:
Allen Linear (Interval) Temporal Logic - Translation to LTL and Monitor Synthesis. 263-277
Electronic Edition (link) BibTeX

Jiri Barnat, Lubos Brim, Ivana Cerná, Pavel Moravec, Petr Rockai, Pavel Simecek:
DiVinE - A Tool for Distributed Verification. 278-281
Electronic Edition (link) BibTeX
Flavio M. de Paula, Alan J. Hu:
EverLost: A Flexible Platform for Industrial-Strength Abstraction-Guided Simulation. 282-285
Electronic Edition (link) BibTeX

Vineet Kahlon, Aarti Gupta, Nishant Sinha:
Symbolic Model Checking of Concurrent Programs Using Partial Orders and On-the-Fly Transactions. 286-299
Electronic Edition (link) BibTeX
Koushik Sen, Mahesh Viswanathan:
Model Checking Multithreaded Programs with Asynchronous Atomic Methods. 300-314
Electronic Edition (link) BibTeX
Azadeh Farzan, P. Madhusudan:
Causal Atomicity. 315-328
Electronic Edition (link) BibTeX

Rajeev Alur, Swarat Chaudhuri, P. Madhusudan:
Languages of Nested Trees. 329-342
Electronic Edition (link) BibTeX
Akash Lal, Thomas W. Reps:
Improving Pushdown System Model Checking. 343-357
Electronic Edition (link) BibTeX
Andreas Griesmayer, Roderick Bloem, Byron Cook:
Repair of Boolean Programs with an Application to C. 358-371
Electronic Edition (link) BibTeX

Mark Braverman:
Termination of Integer Linear Programs. 372-385
Electronic Edition (link) BibTeX
Josh Berdine, Byron Cook, Dino Distefano, Peter W. O'Hearn:
Automatic Termination Proofs for Programs with Shape-Shifting Heaps. 386-400
Electronic Edition (link) BibTeX
Panagiotis Manolios, Daron Vroon:
Termination Analysis with Calling Context Graphs. 401-414
Electronic Edition (link) BibTeX

Byron Cook, Andreas Podelski, Andrey Rybalchenko:
Terminator: Beyond Safety. 415-418
Electronic Edition (link) BibTeX
Koushik Sen, Gul Agha:
CUTE and jCUTE: Concolic Unit Testing and Explicit Path Model-Checking Tools. 419-423
Electronic Edition (link) BibTeX

Kenneth Roe:
The Heuristic Theorem Prover: Yet Another SMT Modulo Theorem Prover. 467-470
Electronic Edition (link) BibTeX
Abhay Vardhan, Mahesh Viswanathan:
LEVER: A Tool for Learning Based Verification. 471-474
Electronic Edition (link) BibTeX

Robert Colvin, Lindsay Groves, Victor Luchangco, Mark Moir:
Formal Verification of a Lazy Concurrent List-Based Set Algorithm. 475-488
Electronic Edition (link) BibTeX
Sebastian Burckhardt, Rajeev Alur, Milo M. K. Martin:
Bounded Model Checking of Concurrent Data Types on Relaxed Memory Models: A Case Study. 489-502
Electronic Edition (link) BibTeX
Amitabha Roy, Stephan Zeisset, Charles J. Fleckenstein, John C. Huang:
Fast and Generalized Polynomial Time Memory Consistency Verification. 503-516
Electronic Edition (link) BibTeX