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

• Συγγραφή απο Οργανισμό/Αρχή: SpringerLink (Online service)
• Άλλοι συγγραφείς: Alur, Rajeev (Επιμελητής έκδοσης), Peled, Doron A. (Επιμελητής έκδοσης)
• Μορφή: Ηλεκτρονική πηγή Ηλ. βιβλίο
• Γλώσσα: English
• Έκδοση: Berlin, Heidelberg : Springer Berlin Heidelberg, 2004.
• Σειρά: Lecture Notes in Computer Science, 3114
• Θέματα: Computer science.; Logic design.; Software engineering.; Computers.; Computer logic.; Mathematical logic.; Artificial intelligence.; Computer Science.; Theory of Computation.; Software Engineering.; Logic Design.; Logics and Meanings of Programs.; Mathematical Logic and Formal Languages.; Artificial Intelligence (incl. Robotics).

Πίνακας περιεχομένων:

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