Proceedings of the 16th 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

Rajeev Alur, Doron Peled
Proceedings of the 16th International Conference on Computer Aided Verification
CAV, 2004.

TEST
DBLP
Scholar
Full names Links ISxN
@proceedings{CAV-2004,
	address       = "Boston, Massachusetts, USA",
	editor        = "Rajeev Alur and Doron Peled",
	isbn          = "3-540-22342-8",
	publisher     = "{Springer International Publishing}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the 16th International Conference on Computer Aided Verification}",
	volume        = 3114,
	year          = 2004,
}

Contents (51 items)

CAV-2004-OLearyR
Rob Tristan Gerth: 1956?2003 (JO, MR), pp. 1–14.
CAV-2004-RepsSW #logic #program analysis
Static Program Analysis via 3-Valued Logic (TWR, SS, RW), pp. 15–30.
CAV-2004-RayH #deduction #first-order #pipes and filters #quantifier #using #verification
Deductive Verification of Pipelined Machines Using First-Order Quantification (SR, WAHJ), pp. 31–43.
CAV-2004-GaoH #algorithm #parallel #reduction
A Formal Reduction for Lock-Free Parallel Algorithms (HG, WHH), pp. 44–56.
CAV-2004-Namjoshi #model checking
An Efficiently Checkable, Proof-Based Formulation of Vacuity in Model Checking (KSN), pp. 57–69.
CAV-2004-Tiwari #linear #source code #termination
Termination of Linear Programs (AT), pp. 70–82.
CAV-2004-Lange #model checking
Symbolic Model Checking of Non-regular Properties (ML), pp. 83–95.
CAV-2004-AwedhS #bound #model checking #proving
Proving More Properties with Bounded Model Checking (MA, FS), pp. 96–108.
CAV-2004-SchroterK #model checking #parallel #petri net
Parallel LTL-X Model Checking of High-Level Petri Nets Based on Unfoldings (CS, VK), pp. 109–121.
CAV-2004-ChangBD #design #interface #refinement #using #verification
Using Interface Refinement to Integrate Formal Verification into the Design Cycle (JC, SB, DLD), pp. 122–134.
CAV-2004-LahiriB #bound #verification
Indexed Predicate Discovery for Unbounded System Verification (SKL, REB), pp. 135–147.
CAV-2004-TalupurSSP #logic
Range Allocation for Separation Logic (MT, NS, OS, AP), pp. 148–161.
CAV-2004-MouraR #evaluation
An Experimental Evaluation of Ground Decision Procedures (LMdM, HR), pp. 162–174.
CAV-2004-GanzingerHNOT #performance
DPLL( T): Fast Decision Procedures (HG, GH, RN, AO, CT), pp. 175–188.
CAV-2004-BustanRV #markov #verification
Verifying ω-Regular Properties of Markov Chains (DB, SR, MYV), pp. 189–201.
CAV-2004-SenVA #black box #model checking #probability #statistics
Statistical Model Checking of Black-Box Probabilistic Systems (KS, MV, GA), pp. 202–215.
CAV-2004-YangS #composition #model checking #specification
Compositional Specification and Model Checking in GSTE (JY, CJHS), pp. 216–228.
CAV-2004-SebastianiSTV #model checking
GSTE Is Partitioned Model Checking (RS, ES, ST, MYV), pp. 229–241.
CAV-2004-FournetHRR #consistency
Stuck-Free Conformance (CF, CARH, SKR, JR), pp. 242–254.
CAV-2004-GoelB #abstraction #functional #model checking #order #simulation
Symbolic Simulation, Model Checking and Abstraction with Partially Ordered Boolean Functional Vectors (AG, REB), pp. 255–267.
CAV-2004-JiangB #dependence #functional #reduction #verification
Functional Dependency for Verification Reduction (JHRJ, RKB), pp. 268–280.
CAV-2004-ImmermanRRSY #simulation #verification
Verification via Structure Simulation (NI, AMR, TWR, SS, GY), pp. 281–294.
CAV-2004-Wang #analysis #hybrid #linear #parametricity #safety
Symbolic Parametric Safety Analysis of Linear Hybrid Systems with BDD-Like Data-Structures (FW), pp. 295–307.
CAV-2004-KroeningOSS #satisfiability
Abstraction-Based Satisfiability Solving of Presburger Arithmetic (DK, JO, SAS, OS), pp. 308–320.
CAV-2004-BartzisB #automaton
Widening Arithmetic Automata (CB, TB), pp. 321–333.
CAV-2004-Metzner #analysis #model checking #why
Why Model Checking Can Improve WCET Analysis (AM), pp. 334–347.
CAV-2004-AbdullaJNdS #ltl #model checking
Regular Model Checking for LTL(MSO) (PAA, BJ, MN, Jd, MS), pp. 348–360.
CAV-2004-FinkelL #image #infinity #model checking
Image Computation in Infinite State Model Checking (AF, JL), pp. 361–371.
CAV-2004-BouajjaniHV #model checking
Abstract Regular Model Checking (AB, PH, TV), pp. 372–386.
CAV-2004-PitermanV #infinity #model checking
Global Model-Checking of Infinite-State Systems (NP, MYV), pp. 387–400.
CAV-2004-GopalakrishnanYS #execution #memory management #order #performance #verification
QB or Not QB: An Efficient Execution Verification Tool for Memory Orderings (GG, YY, HS), pp. 401–413.
CAV-2004-Arons #algorithm #execution #verification
Verification of an Advanced mips-Type Out-of-Order Execution Algorithm (TA), pp. 414–426.
CAV-2004-BinghamCHQZ #automation #bound #consistency #verification
Automatic Verification of Sequential Consistency for Unbounded Addresses and Data Values (JDB, AC, AJH, SQ, ZZ), pp. 427–439.
CAV-2004-GanaiGA #bound #embedded #model checking #modelling #performance
Efficient Modeling of Embedded Memories in Bounded Model Checking (MKG, AG, PA), pp. 440–452.
CAV-2004-GroceKL #comprehension
Understanding Counterexamples with explain (AG, DK, FL), pp. 453–456.
CAV-2004-BallCLZ #abstraction #automation #named #proving #refinement #theorem proving
Zapato: Automatic Theorem Proving for Predicate Abstraction Refinement (TB, BC, SKL, LZ), pp. 457–461.
CAV-2004-ArthoSBEBZ #dynamic analysis #java #named #performance
JNuke: Efficient Dynamic Analysis for Java (CA, VS, AB, PE, MB, BZ), pp. 462–465.
CAV-2004-PingreeM #set
The HiVy Tool Set (PJP, EM), pp. 466–469.
CAV-2004-BrabermanGO #automaton #named #slicing
ObsSlice: A Timed Automata Slicer Based on Observers (VAB, DG, AO), pp. 470–474.
CAV-2004-LahiriS
The UCLID Decision Procedure (SKL, SAS), pp. 475–478.
CAV-2004-GammieM #logic #model checking #named
MCK: Model Checking the Logic of Knowledge (PG, RvdM), pp. 479–483.
CAV-2004-AndrewsQRRX #concurrent #model checking #named
Zing: A Model Checker for Concurrent Software (TA, SQ, SKR, JR, YX), pp. 484–487.
CAV-2004-GriffaultV #model checking
The Mec 5 Model-Checker (AG, AV), pp. 488–491.
CAV-2004-Tan #framework #game studies #named #platform
PlayGame: A Platform for Diagnostic Games (LT), pp. 492–495.
CAV-2004-MouraORRSST
SAL 2 (LMdM, SO, HR, JMR, NS, MS, AT), pp. 496–500.
CAV-2004-FarzanCMR #analysis #formal method #java #source code
Formal Analysis of Java Programs in JavaFAN (AF, FC, JM, GR), pp. 501–505.
CAV-2004-RameshSDCV #modelling #tool support #verification
A Toolset for Modelling and Verification of GALS Systems (SR, SS, VD, NC, BV), pp. 506–509.
CAV-2004-FuBS #analysis #formal method #named #web #web service
WSAT: A Tool for Formal Analysis of Web Services (XF, TB, JS), pp. 510–514.
CAV-2004-BarrettB #implementation
CVC Lite: A New Implementation of the Cooperating Validity Checker Category B (CWB, SB), pp. 515–518.
CAV-2004-JinAS #bound #model checking #named #satisfiability #towards
CirCUs: A Satisfiability Solver Geared towards Bounded Model Checking (HJ, MA, FS), pp. 519–522.
CAV-2004-Hunt #verification
Mechanical Mathematical Methods for Microprocessor Verification (WAHJ), pp. 523–533.

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.