18. CAV 2006: Seattle, WA, USA

Invited Talks

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

Automata

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

Tool Papers

• B. Thomas Adler, Luca de Alfaro, Leandro Dias da Silva, Marco Faella, Axel Legay, Vishwanath Raman, Pritam Roy:
  Ticc: A Tool for Interface Compatibility and Composition. 59-62
  
• Sébastien Bardin, Jérôme Leroux, Gérald Point:
  FAST Extended Release. 63-66
  

Arithmetic

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

SAT and Bounded Model Checking

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

Abstraction/Refinement

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

Tool Papers

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

Symbolic Trajectory Evaluation

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

Property Specification and Verification

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

Time

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

Tool Papers

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

Concurrency

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

Trees, Pushdown Systems and Boolean Programs

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

Termination

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

Tool Papers

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

Abstract Interpretation

• Shuvendu K. Lahiri, Robert Nieuwenhuis, Albert Oliveras:
  SMT Techniques for Fast Predicate Abstraction. 424-437
  
• Bernard Boigelot, Frédéric Herbreteau:
  The Power of Hybrid Acceleration. 438-451
  
• Denis Gopan, Thomas W. Reps:
  Lookahead Widening. 452-466
  

Tool Papers

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

Memory Consistency

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

Shape Analysis

• Ahmed Bouajjani, Marius Bozga, Peter Habermehl, Radu Iosif, Pierre Moro, Tomás Vojnar:
  Programs with Lists Are Counter Automata. 517-531
  
• Dirk Beyer, Thomas A. Henzinger, Grégory Théoduloz:
  Lazy Shape Analysis. 532-546
  
• Tal Lev-Ami, Neil Immerman, Shmuel Sagiv:
  Abstraction for Shape Analysis with Fast and Precise Transformers. 547-561