CAV 2006

49 papers

1. A Fast Linear-Arithmetic Solver for DPLL(T) · Bruno Dutertre, Leonardo Mendonça de Moura
2. Abstraction for Shape Analysis with Fast and Precise Transformers · Tal Lev-Ami, Neil Immerman, Shmuel Sagiv
3. Allen Linear (Interval) Temporal Logic - Translation to LTL and Monitor Synthesis · Grigore Rosu, Saddek Bensalem
4. Antichains: A New Algorithm for Checking Universality of Finite Automata · Martin De Wulf, Laurent Doyen, Thomas A. Henzinger, Jean-François Raskin
5. Automatic Refinement and Vacuity Detection for Symbolic Trajectory Evaluation · Rachel Tzoref, Orna Grumberg
6. Automatic Termination Proofs for Programs with Shape-Shifting Heaps · Josh Berdine, Byron Cook, Dino Distefano, Peter W. O'Hearn
7. Bounded Model Checking for Weak Alternating Büchi Automata · Keijo Heljanko, Tommi A. Junttila, Misa Keinänen, Martin Lange, Timo Latvala
8. Bounded Model Checking of Concurrent Data Types on Relaxed Memory Models: A Case Study · Sebastian Burckhardt, Rajeev Alur, Milo M. K. Martin
9. CUTE and jCUTE: Concolic Unit Testing and Explicit Path Model-Checking Tools · Koushik Sen, Gul Agha
10. Causal Atomicity · Azadeh Farzan, P. Madhusudan
11. Check It Out: On the Efficient Formal Verification of Live Sequence Charts · Jochen Klose, Tobe Toben, Bernd Westphal, Hartmut Wittke
12. Communicating Timed Automata: The More Synchronous, the More Difficult to Verify · Pavel Krcál, Wang Yi
13. Counterexamples with Loops for Predicate Abstraction · Daniel Kroening, Georg Weissenbacher
14. Deriving Small Unsatisfiable Cores with Dominators · Roman Gershman, Maya Koifman, Ofer Strichman
15. DiVinE - A Tool for Distributed Verification · Jiri Barnat, Lubos Brim, Ivana Cerná, Pavel Moravec, Petr Rockai, Pavel Simecek
16. Don't Care Words with an Application to the Automata-Based Approach for Real Addition · Jochen Eisinger, Felix Klaedtke
17. EverLost: A Flexible Platform for Industrial-Strength Abstraction-Guided Simulation · Flavio M. de Paula, Alan J. Hu
18. FAST Extended Release · Sébastien Bardin, Jérôme Leroux, Gérald Point
19. Fast and Generalized Polynomial Time Memory Consistency Verification · Amitabha Roy, Stephan Zeisset, Charles J. Fleckenstein, John C. Huang
20. Formal Specifications on Industrial-Strength Code-From Myth to Reality · Manuvir Das
21. Formal Verification of a Lazy Concurrent List-Based Set Algorithm · Robert Colvin, Lindsay Groves, Victor Luchangco, Mark Moir
22. I Think I Voted: E-Voting vs. Democracy · David L. Dill
23. Improving Pushdown System Model Checking · Akash Lal, Thomas W. Reps
24. LEVER: A Tool for Learning Based Verification · Abhay Vardhan, Mahesh Viswanathan
25. Languages of Nested Trees · Rajeev Alur, Swarat Chaudhuri, P. Madhusudan
26. Lazy Abstraction with Interpolants · Kenneth L. McMillan
27. Lazy Shape Analysis · Dirk Beyer, Thomas A. Henzinger, Grégory Théoduloz
28. Lookahead Widening · Denis Gopan, Thomas W. Reps
29. Minimizing Generalized Büchi Automata · Sudeep Juvekar, Nir Piterman
30. Model Checking Multithreaded Programs with Asynchronous Atomic Methods · Koushik Sen, Mahesh Viswanathan
31. Playing with Verification, Planning and Aspects: Unusual Methods for Running Scenario-Based Programs · David Harel
32. Programs with Lists Are Counter Automata · Ahmed Bouajjani, Marius Bozga, Peter Habermehl, Radu Iosif, Pierre Moro, Tomás Vojnar
33. Repair of Boolean Programs with an Application to C · Andreas Griesmayer, Roderick Bloem, Byron Cook
34. SAT-Based Assistance in Abstraction Refinement for Symbolic Trajectory Evaluation · Jan-Willem Roorda, Koen Claessen
35. SMT Techniques for Fast Predicate Abstraction · Shuvendu K. Lahiri, Robert Nieuwenhuis, Albert Oliveras
36. Safraless Compositional Synthesis · Orna Kupferman, Nir Piterman, Moshe Y. Vardi
37. Some Complexity Results for SystemVerilog Assertions · Doron Bustan, John Havlicek
38. Symbolic Model Checking of Concurrent Programs Using Partial Orders and On-the-Fly Transactions · Vineet Kahlon, Aarti Gupta, Nishant Sinha
39. Symmetry Reduction for Probabilistic Model Checking · Marta Z. Kwiatkowska, Gethin Norman, David Parker
40. Termination Analysis with Calling Context Graphs · Panagiotis Manolios, Daron Vroon
41. Termination of Integer Linear Programs · Mark Braverman
42. Terminator: Beyond Safety · Byron Cook, Andreas Podelski, Andrey Rybalchenko
43. The Heuristic Theorem Prover: Yet Another SMT Modulo Theorem Prover · Kenneth Roe
44. The Ideal of Verified Software · Tony Hoare
45. The Power of Hybrid Acceleration · Bernard Boigelot, Frédéric Herbreteau
46. Ticc: A Tool for Interface Compatibility and Composition · B. Thomas Adler, Luca de Alfaro, Leandro Dias da Silva, Marco Faella, Axel Legay, Vishwanath Raman + 1 more
47. Using Statically Computed Invariants Inside the Predicate Abstraction and Refinement Loop · Himanshu Jain, Franjo Ivancic, Aarti Gupta, Ilya Shlyakhter, Chao Wang
48. Yasm: A Software Model-Checker for Verification and Refutation · Arie Gurfinkel, Ou Wei, Marsha Chechik
49. cascade: C Assertion Checker and Deductive Engine · Nikhil Sethi, Clark W. Barrett