Computer Aided Verification 16th International Conference, CAV 2004, Boston, MA, USA, July 13-17, 2004, Proceedings

Computer Aided Verification 16th International Conference, CAV 2004, Boston, MA, USA, July 13-17, 2004, Proceedings / edited by Rajeev Alur, Doron A. Peled.

Saved in:
Bibliographic Details
Corporate Author: SpringerLink (Online service)
Other Authors: Alur, Rajeev (Editor), Peled, Doron A. (Editor)
Format: eBook
Language:English
Published: Berlin, Heidelberg : Springer Berlin Heidelberg : Imprint: Springer, 2004.
Edition:1st ed. 2004.
Series:Lecture Notes in Computer Science, 3114
Springer eBook Collection.
Subjects:
Computers.
Software engineering.
Logic design.
Computer logic.
Mathematical logic.
Artificial intelligence.
Electronic resources (E-books)
Online Access:Click to view e-book
Holy Cross Note:Loaded electronically.
Electronic access restricted to members of the Holy Cross Community.
Table of 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.

Similar Items