Coverart for item
The Resource Computer aided verification : 16th international conference, CAV 2004, Boston, MA, USA, July 13-17, 2004 ; proceedings, Rajeev Alur, Doron A. Peled (eds.)

Computer aided verification : 16th international conference, CAV 2004, Boston, MA, USA, July 13-17, 2004 ; proceedings, Rajeev Alur, Doron A. Peled (eds.)

Label
Computer aided verification : 16th international conference, CAV 2004, Boston, MA, USA, July 13-17, 2004 ; proceedings
Title
Computer aided verification
Title remainder
16th international conference, CAV 2004, Boston, MA, USA, July 13-17, 2004 ; proceedings
Statement of responsibility
Rajeev Alur, Doron A. Peled (eds.)
Title variation
CAV 2004
Creator
Contributor
Subject
Genre
Language
eng
Summary
This book constitutes the refereed proceedings of the 16th International Conference on Computer Aided Verification, CAV 2004, held in Boston, MA, USA, in July 2004. The 32 revised full research papers and 16 tool papers were carefully reviewed and selected from 144 submissions. The papers cover all current issues in computer aided verification and model checking, ranging from foundational and methodological issues to the evaluation of major tools and systems
Member of
Cataloging source
N$T
Dewey number
004.24
Index
index present
LC call number
QA76.76.V47
LC item number
C38 2004eb
Literary form
non fiction
http://bibfra.me/vocab/lite/meetingDate
2004
http://bibfra.me/vocab/lite/meetingName
CAV (Conference)
Nature of contents
  • dictionaries
  • bibliography
http://library.link/vocab/relatedWorkOrContributorDate
  • 1966-
  • 1962-
http://library.link/vocab/relatedWorkOrContributorName
  • Alur, Rajeev
  • Peled, Doron A.
Series statement
Lecture notes in computer science,
Series volume
3114
http://library.link/vocab/subjectName
  • Computer software
  • Integrated circuits
  • Electronic digital computers
  • COMPUTERS
  • Computer software
  • Electronic digital computers
  • Integrated circuits
Label
Computer aided verification : 16th international conference, CAV 2004, Boston, MA, USA, July 13-17, 2004 ; proceedings, Rajeev Alur, Doron A. Peled (eds.)
Instantiates
Publication
Antecedent source
unknown
Bibliography note
Includes bibliographical references and index
Carrier category
online resource
Carrier category code
  • cr
Carrier MARC source
rdacarrier
Color
multicolored
Content category
text
Content type code
  • txt
Content type MARC source
rdacontent
Contents
Rob Tristan Gerth: 1956-2003 -- Static Program Analysis via 3-Valued Logic -- Deductive Verification of Pipelined Machines Using First-Order Quantification -- A Formal Reduction for Lock-Free Parallel Algorithms -- An Efficiently Checkable, Proof-Based Formulation of Vacuity in Model Checking -- Termination of Linear Programs -- Symbolic Model Checking of Non-regular Properties -- Proving More Properties with Bounded Model Checking -- Parallel LTL-X Model Checking of High-Level Petri Nets Based on Unfoldings -- Using Interface Refinement to Integrate Formal Verification into the Design Cycle -- Indexed Predicate Discovery for Unbounded System Verification -- Range Allocation for Separation Logic -- An Experimental Evaluation of Ground Decision Procedures -- DPLL(T): Fast Decision Procedures -- Verifying?-Regular Properties of Markov Chains -- Statistical Model Checking of Black-Box Probabilistic Systems -- Compositional Specification and Model Checking in GSTE -- GSTE Is Partitioned Model Checking -- Stuck-Free Conformance -- Symbolic Simulation, Model Checking and Abstraction with Partially Ordered Boolean Functional Vectors -- Functional Dependency for Verification Reduction -- Verification via Structure Simulation -- Symbolic Parametric Safety Analysis of Linear Hybrid Systems with BDD-Like Data-Structures -- Abstraction-Based Satisfiability Solving of Presburger Arithmetic -- Widening Arithmetic Automata -- Why Model Checking Can Improve WCET Analysis -- Regular Model Checking for LTL(MSO) -- Image Computation in Infinite State Model Checking -- Abstract Regular Model Checking -- Global Model-Checking of Infinite-State Systems -- QB or Not QB: An Efficient Execution Verification Tool for Memory Orderings -- Verification of an Advanced mips-Type Out-of-Order Execution Algorithm -- Automatic Verification of Sequential Consistency for Unbounded Addresses and Data Values -- Efficient Modeling of Embedded Memories in Bounded Model Checking -- Understanding Counterexamples with explain -- Zapato: Automatic Theorem Proving for Predicate Abstraction Refinement -- JNuke: Efficient Dynamic Analysis for Java -- The HiVy Tool Set -- ObsSlice: A Timed Automata Slicer Based on Observers -- The UCLID Decision Procedure -- MCK: Model Checking the Logic of Knowledge -- Zing: A Model Checker for Concurrent Software -- The Mec 5 Model-Checker -- PlayGame: A Platform for Diagnostic Games -- SAL 2 -- Formal Analysis of Java Programs in JavaFAN -- A Toolset for Modelling and Verification of GALS Systems -- WSAT: A Tool for Formal Analysis of Web Services -- CVC Lite: A New Implementation of the Cooperating Validity Checker -- CirCUs: A Satisfiability Solver Geared towards Bounded Model Checking -- Mechanical Mathematical Methods for Microprocessor Verification
Control code
60785831
Dimensions
unknown
Extent
1 online resource (xii, 536 pages)
File format
unknown
Form of item
online
Isbn
9783540278139
Level of compression
unknown
Media category
computer
Media MARC source
rdamedia
Media type code
  • c
Other control number
10.1007/b98490
Other physical details
figure, table.
Quality assurance targets
not applicable
Reformatting quality
unknown
Sound
unknown sound
Specific material designation
remote
System control number
(OCoLC)60785831
Label
Computer aided verification : 16th international conference, CAV 2004, Boston, MA, USA, July 13-17, 2004 ; proceedings, Rajeev Alur, Doron A. Peled (eds.)
Publication
Antecedent source
unknown
Bibliography note
Includes bibliographical references and index
Carrier category
online resource
Carrier category code
  • cr
Carrier MARC source
rdacarrier
Color
multicolored
Content category
text
Content type code
  • txt
Content type MARC source
rdacontent
Contents
Rob Tristan Gerth: 1956-2003 -- Static Program Analysis via 3-Valued Logic -- Deductive Verification of Pipelined Machines Using First-Order Quantification -- A Formal Reduction for Lock-Free Parallel Algorithms -- An Efficiently Checkable, Proof-Based Formulation of Vacuity in Model Checking -- Termination of Linear Programs -- Symbolic Model Checking of Non-regular Properties -- Proving More Properties with Bounded Model Checking -- Parallel LTL-X Model Checking of High-Level Petri Nets Based on Unfoldings -- Using Interface Refinement to Integrate Formal Verification into the Design Cycle -- Indexed Predicate Discovery for Unbounded System Verification -- Range Allocation for Separation Logic -- An Experimental Evaluation of Ground Decision Procedures -- DPLL(T): Fast Decision Procedures -- Verifying?-Regular Properties of Markov Chains -- Statistical Model Checking of Black-Box Probabilistic Systems -- Compositional Specification and Model Checking in GSTE -- GSTE Is Partitioned Model Checking -- Stuck-Free Conformance -- Symbolic Simulation, Model Checking and Abstraction with Partially Ordered Boolean Functional Vectors -- Functional Dependency for Verification Reduction -- Verification via Structure Simulation -- Symbolic Parametric Safety Analysis of Linear Hybrid Systems with BDD-Like Data-Structures -- Abstraction-Based Satisfiability Solving of Presburger Arithmetic -- Widening Arithmetic Automata -- Why Model Checking Can Improve WCET Analysis -- Regular Model Checking for LTL(MSO) -- Image Computation in Infinite State Model Checking -- Abstract Regular Model Checking -- Global Model-Checking of Infinite-State Systems -- QB or Not QB: An Efficient Execution Verification Tool for Memory Orderings -- Verification of an Advanced mips-Type Out-of-Order Execution Algorithm -- Automatic Verification of Sequential Consistency for Unbounded Addresses and Data Values -- Efficient Modeling of Embedded Memories in Bounded Model Checking -- Understanding Counterexamples with explain -- Zapato: Automatic Theorem Proving for Predicate Abstraction Refinement -- JNuke: Efficient Dynamic Analysis for Java -- The HiVy Tool Set -- ObsSlice: A Timed Automata Slicer Based on Observers -- The UCLID Decision Procedure -- MCK: Model Checking the Logic of Knowledge -- Zing: A Model Checker for Concurrent Software -- The Mec 5 Model-Checker -- PlayGame: A Platform for Diagnostic Games -- SAL 2 -- Formal Analysis of Java Programs in JavaFAN -- A Toolset for Modelling and Verification of GALS Systems -- WSAT: A Tool for Formal Analysis of Web Services -- CVC Lite: A New Implementation of the Cooperating Validity Checker -- CirCUs: A Satisfiability Solver Geared towards Bounded Model Checking -- Mechanical Mathematical Methods for Microprocessor Verification
Control code
60785831
Dimensions
unknown
Extent
1 online resource (xii, 536 pages)
File format
unknown
Form of item
online
Isbn
9783540278139
Level of compression
unknown
Media category
computer
Media MARC source
rdamedia
Media type code
  • c
Other control number
10.1007/b98490
Other physical details
figure, table.
Quality assurance targets
not applicable
Reformatting quality
unknown
Sound
unknown sound
Specific material designation
remote
System control number
(OCoLC)60785831

Library Locations

    • Ellis LibraryBorrow it
      1020 Lowry Street, Columbia, MO, 65201, US
      38.944491 -92.326012
Processing Feedback ...