Proceedings of the 18th International Conference on Computer Aided Verification
BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
EDIT!
CC-BY
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter

Thomas Ball, Robert B. Jones
Proceedings of the 18th International Conference on Computer Aided Verification
CAV, 2006.

TEST
DBLP
Scholar
Full names Links ISxN
@proceedings{CAV-2006,
	address       = "Seattle, Washington, USA",
	editor        = "Thomas Ball and Robert B. Jones",
	isbn          = "3-540-37406-X",
	publisher     = "{Springer International Publishing}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the 18th International Conference on Computer Aided Verification}",
	volume        = 4144,
	year          = 2006,
}

Contents (49 items)

CAV-2006-Das #specification
Formal Specifications on Industrial-Strength Code-From Myth to Reality (MD), p. 1.
CAV-2006-Dill
I Think I Voted: E-Voting vs. Democracy (DLD), p. 2.
CAV-2006-Harel #aspect-oriented #game studies #source code #verification
Playing with Verification, Planning and Aspects: Unusual Methods for Running Scenario-Based Programs (DH), pp. 3–4.
CAV-2006-Hoare
The Ideal of Verified Software (CARH), pp. 5–16.
CAV-2006-WulfDHR #algorithm #anti #automaton #finite #named
Antichains: A New Algorithm for Checking Universality of Finite Automata (MDW, LD, TAH, JFR), pp. 17–30.
CAV-2006-KupfermanPV #composition #synthesis
Safraless Compositional Synthesis (OK, NP, MYV), pp. 31–44.
CAV-2006-JuvekarP #automaton
Minimizing Generalized Büchi Automata (SJ, NP), pp. 45–58.
CAV-2006-AdlerASFLRR #composition #interface #named
Ticc: A Tool for Interface Compatibility and Composition (BTA, LdA, LDdS, MF, AL, VR, PR), pp. 59–62.
CAV-2006-BardinLP #performance
FAST Extended Release (SB, JL, GP), pp. 63–66.
CAV-2006-EisingerK #approach #word
Don’t Care Words with an Application to the Automata-Based Approach for Real Addition (JE, FK), pp. 67–80.
CAV-2006-DutertreM #performance
A Fast Linear-Arithmetic Solver for DPLL(T) (BD, LMdM), pp. 81–94.
CAV-2006-HeljankoJKLL #automaton #bound #model checking
Bounded Model Checking for Weak Alternating Büchi Automata (KH, TAJ, MK, ML, TL), pp. 95–108.
CAV-2006-GershmanKS #satisfiability
Deriving Small Unsatisfiable Cores with Dominators (RG, MK, OS), pp. 109–122.
CAV-2006-McMillan #abstraction #lazy evaluation
Lazy Abstraction with Interpolants (KLM), pp. 123–136.
CAV-2006-JainIGSW #abstraction #invariant #refinement #using
Using Statically Computed Invariants Inside the Predicate Abstraction and Refinement Loop (HJ, FI, AG, IS, CW), pp. 137–151.
CAV-2006-KroeningW #abstraction
Counterexamples with Loops for Predicate Abstraction (DK, GW), pp. 152–165.
CAV-2006-SethiB #c #deduction #named
cascade: C Assertion Checker and Deductive Engine (NS, CB), pp. 166–169.
CAV-2006-GurfinkelWC #model checking #named #verification
Yasm: A Software Model-Checker for Verification and Refutation (AG, OW, MC), pp. 170–174.
CAV-2006-RoordaC #abstraction #evaluation #refinement #satisfiability
SAT-Based Assistance in Abstraction Refinement for Symbolic Trajectory Evaluation (JWR, KC), pp. 175–189.
CAV-2006-TzorefG #automation #detection #evaluation #refinement
Automatic Refinement and Vacuity Detection for Symbolic Trajectory Evaluation (RT, OG), pp. 190–204.
CAV-2006-BustanH #complexity
Some Complexity Results for SystemVerilog Assertions (DB, JH), pp. 205–218.
CAV-2006-KloseTWW #performance #sequence chart #verification
Check It Out: On the Efficient Formal Verification of Live Sequence Charts (JK, TT, BW, HW), pp. 219–233.
CAV-2006-KwiatkowskaNP #model checking #probability #reduction #symmetry
Symmetry Reduction for Probabilistic Model Checking (MZK, GN, DP), pp. 234–248.
CAV-2006-KrcalY #automaton #communication #verification
Communicating Timed Automata: The More Synchronous, the More Difficult to Verify (PK, WY), pp. 249–262.
CAV-2006-RosuB #linear #logic #ltl #monitoring #synthesis
Allen Linear (Interval) Temporal Logic — Translation to LTL and Monitor Synthesis (GR, SB), pp. 263–277.
CAV-2006-BarnatBCMRS #distributed #named #verification
DiVinE — A Tool for Distributed Verification (JB, LB, IC, PM, PR, PS), pp. 278–281.
CAV-2006-PaulaH #flexibility #framework #named #platform #simulation
EverLost: A Flexible Platform for Industrial-Strength Abstraction-Guided Simulation (FMdP, AJH), pp. 282–285.
CAV-2006-KahlonGS #concurrent #model checking #on the fly #partial order #source code #transaction #using
Symbolic Model Checking of Concurrent Programs Using Partial Orders and On-the-Fly Transactions (VK, AG, NS), pp. 286–299.
CAV-2006-SenV #model checking #parallel #source code #thread
Model Checking Multithreaded Programs with Asynchronous Atomic Methods (KS, MV), pp. 300–314.
CAV-2006-FarzanM
Causal Atomicity (AF, PM), pp. 315–328.
CAV-2006-AlurCM
Languages of Nested Trees (RA, SC, PM), pp. 329–342.
CAV-2006-LalR #automaton #model checking
Improving Pushdown System Model Checking (AL, TWR), pp. 343–357.
CAV-2006-GriesmayerBC #c #source code
Repair of Boolean Programs with an Application to C (AG, RB, BC), pp. 358–371.
CAV-2006-Braverman #integer #linear #source code #termination
Termination of Integer Linear Programs (MB), pp. 372–385.
CAV-2006-BerdineCDO #automation #proving #source code #termination
Automatic Termination Proofs for Programs with Shape-Shifting Heaps (JB, BC, DD, PWO), pp. 386–400.
CAV-2006-ManoliosV #analysis #graph #termination
Termination Analysis with Calling Context Graphs (PM, DV), pp. 401–414.
CAV-2006-CookPR #named #safety
Terminator: Beyond Safety (BC, AP, AR), pp. 415–418.
CAV-2006-SenA #model checking #testing #tool support
CUTE and jCUTE: Concolic Unit Testing and Explicit Path Model-Checking Tools (KS, GA), pp. 419–423.
CAV-2006-LahiriNO #abstraction #performance #smt
SMT Techniques for Fast Predicate Abstraction (SKL, RN, AO), pp. 424–437.
CAV-2006-BoigelotH #hybrid #power of
The Power of Hybrid Acceleration (BB, FH), pp. 438–451.
CAV-2006-GopanR #lookahead
Lookahead Widening (DG, TWR), pp. 452–466.
CAV-2006-Roe #heuristic #modulo theories #proving #smt #theorem proving
The Heuristic Theorem Prover: Yet Another SMT Modulo Theorem Prover (KR), pp. 467–470.
CAV-2006-VardhanV #learning #named #verification
LEVER: A Tool for Learning Based Verification (AV, MV), pp. 471–474.
CAV-2006-ColvinGLM #algorithm #concurrent #lazy evaluation #set #verification
Formal Verification of a Lazy Concurrent List-Based Set Algorithm (RC, LG, VL, MM), pp. 475–488.
CAV-2006-BurckhardtAM #bound #case study #concurrent #data type #memory management #model checking #modelling
Bounded Model Checking of Concurrent Data Types on Relaxed Memory Models: A Case Study (SB, RA, MMKM), pp. 489–502.
CAV-2006-RoyZFH #consistency #memory management #performance #polynomial #verification
Fast and Generalized Polynomial Time Memory Consistency Verification (AR, SZ, CJF, JCH), pp. 503–516.
CAV-2006-BouajjaniBHIMV #automaton #source code
Programs with Lists Are Counter Automata (AB, MB, PH, RI, PM, TV), pp. 517–531.
CAV-2006-BeyerHT #analysis #lazy evaluation
Lazy Shape Analysis (DB, TAH, GT), pp. 532–546.
CAV-2006-Lev-AmiIS #abstraction #analysis #performance #precise
Abstraction for Shape Analysis with Fast and Precise Transformers (TLA, NI, SS), pp. 547–561.

Bibliography of Software Language Engineering in Generated Hypertext (BibSLEIGH) is created and maintained by Dr. Vadim Zaytsev.
Hosted as a part of SLEBOK on GitHub.