BibSLEIGH — Proceedings of the 18th International Conference on Computer Aided Verification

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

TEST

@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.

Thomas Ball, Robert B. JonesProceedings of the 18th International Conference on Computer Aided VerificationCAV, 2006.

Contents (49 items)

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