default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID18th CAV 2006: Seattle, WA, USA
- Thomas Ball, Robert B. Jones:
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
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 W. 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
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
last updated on 2025-01-15 20:34 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
