计算机辅助验证 Computer aided verification

出版时间：2002-12  出版社：1 (2002年9月1日)  作者：Ed Brinksma  页数：626  

内容概要

This book constitutes the refereed proceedings of the 14th International Conference on Computer Aided Verification, CAV 2002, held in Copenhagen, Denmark in July 2002. The 35 revised full papers presented together with five invited contributions and 11 tool presentations were carefully reviewed and selected from 94 submissions. The papers are organized in topical sections in symbolic model checking, abstraction/refinement and model checking, compositional/structural verification, timing analysis, SAT based methods, infinite state model checking, extended model checking, code verification, regular model checking and acceleration, and model reduction.

书籍目录

Invited Talks　Software Analysis and Model Checking　The Quest for Efficient Boolean Satisfiability SolversInvited Tutorials　On Abstraction in Software Verification　The Symbolic Approach to Hybrid Systems　Infinite Games and Verification (Extended Abstract of a Tutorial)Symbolic Model Checking　Symbolic Localization Reduction with Reconstruction Layering and Backtracking　Modeling and Verifying Systems Using a Logic of Counter Arithmetic with Lambda Expressions and 　Uninterpreted Functions　Combining Symmetry Reduction and Under-Approximation for Symbolic Model CheckingAbstraction/Refinement and Model Checking　Liveness with (0, 1, oc)-Counter Abstraction　Shared Memory Consistency Protocol Verification Against Weak Memory Models: Refinement via Model-Checking　Automatic Abstraction Using Generalized Model CheckingCompositional/Structural Verification　Property Checking via Structural Analysis　Conformance Checking for Models of Asynchronous Message Passing Software　A Modular Checker for Multithreaded ProgramsTiming Analysis　Automatic Derivation of Timing Constraints by Failure Analysis　Deciding Separation Formulas with SAT　Probabilistic Verification of Discrete Event Systems Using Acceptance SamplingSAT Based Methods　Checking Satisfiability of First-Order Formulas by Incremental Translation to SAT　Applying SAT Methods in Unbounded Symbolic Model Checking　SAT Based Abstraction-Refinement Using ILP and Machine Learning Techniques　Semi-formal Bounded Model CheckingSymbolic Model Checking　Algorithmic Verification of Invalidation-Based Protocols　Formal Verification of Complex Out-of-Order Pipelines by Combining Model-Checking and Theorem-Proving……Tool PresentationsExtended Model CheckingTool PresentationsCode VerificationRegular Model Checking and AccelerationModel ReaductionAuthor Index