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

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

TEST

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

Rajeev Alur, Doron PeledProceedings of the 16th International Conference on Computer Aided VerificationCAV, 2004.

Contents (51 items)

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