Computer aided verification : 17th international conference, CAV 2005, Edinburgh, Scotland, UK, July 6-10, 2005 : proceedings, Kousha Etessami, Sriram K. Rajamani (eds.)

Resource Information

The instance Computer aided verification : 17th international conference, CAV 2005, Edinburgh, Scotland, UK, July 6-10, 2005 : proceedings, Kousha Etessami, Sriram K. Rajamani (eds.) represents a material embodiment of a distinct intellectual or artistic creation found in University of Missouri Libraries. This resource is a combination of several types including: Instance, Electronic.

Image

http://images.btol.com/ContentCafe/Jacket.aspx?UserID=ebsco-test&Password=ebsco-test&Return=T&Value=9783540316862&Type=L

Label

Computer aided verification : 17th international conference, CAV 2005, Edinburgh, Scotland, UK, July 6-10, 2005 : proceedings, Kousha Etessami, Sriram K. Rajamani (eds.)

Title remainder

17th international conference, CAV 2005, Edinburgh, Scotland, UK, July 6-10, 2005 : proceedings

Statement of responsibility

Kousha Etessami, Sriram K. Rajamani (eds.)

Instantiates

• Computer aided verification : 17th international conference, CAV 2005, Edinburgh, Scotland, UK, July 6-10, 2005 : proceedings

Publication

• Berlin | New York, Springer, 2005

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

Invited Talks -- Randomized Algorithms for Program Analysis and Verification -- Validating a Modern Microprocessor -- Algorithmic Algebraic Model Checking I: Challenges from Systems Biology -- Tools Competition -- SMT-COMP: Satisfiability Modulo Theories Competition -- Abstraction and Refinement -- Predicate Abstraction via Symbolic Decision Procedures -- Interpolant-Based Transition Relation Approximation -- Concrete Model Checking with Abstract Matching and Refinement -- Abstraction for Falsification -- Bounded Model Checking -- Bounded Model Checking of Concurrent Programs -- Incremental and Complete Bounded Model Checking for Full PLTL -- Abstraction Refinement for Bounded Model Checking -- Symmetry Reduction in SAT-Based Model Checking -- Tool Papers I -- Saturn: A SAT-Based Tool for Bug Detection -- JVer: A Java Verifier -- Building Your Own Software Model Checker Using the Bogor Extensible Model Checking Framework -- Wolf -- Bug Hunter for Concurrent Software Using Formal Methods -- Model Checking x86 Executables with CodeSurfer/x86 and WPDS++ -- The ComFoRT Reasoning Framework -- Verification of Hardware, Microcode, and Synchronous Systems -- Formal Verification of Pentium ® 4 Components with Symbolic Simulation and Inductive Invariants -- Formal Verification of Backward Compatibility of Microcode -- Compositional Analysis of Floating-Point Linear Numerical Filters -- Syntax-Driven Reachable State Space Construction of Synchronous Reactive Programs -- Games and Probabilistic Verification -- Program Repair as a Game -- Improved Probabilistic Models for 802.11 Protocol Verification -- Probabilistic Verification for "Black-Box" Systems -- On Statistical Model Checking of Stochastic Systems -- Tool Papers II -- The AVISPA Tool for the Automated Validation of Internet Security Protocols and Applications -- The Orchids Intrusion Detection Tool -- TVOC: A Translation Validator for Optimizing Compilers -- Cogent: Accurate Theorem Proving for Program Verification -- F-Soft: Software Verification Platform -- Decision Procedures and Applications -- Yet Another Decision Procedure for Equality Logic -- DPLL(T) with Exhaustive Theory Propagation and Its Application to Difference Logic -- Efficient Satisfiability Modulo Theories via Delayed Theory Combination -- Automata and Transition Systems -- Symbolic Systems, Explicit Properties: On Hybrid Approaches for LTL Symbolic Model Checking -- Efficient Monitoring of?-Languages -- Verification of Tree Updates for Optimization -- Expand, Enlarge and Check ... Made Efficient -- Tool Papers III -- IIV: An Invisible Invariant Verifier -- Action Language Verifier, Extended -- Romeo: A Tool for Analyzing Time Petri Nets -- TRANSYT:A Tool for the Verification of Asynchronous Concurrent Systems -- Ymer: A Statistical Model Checker -- Program Analysis and Verification I -- Extended Weighted Pushdown Systems -- Incremental Algorithms for Inter-procedural Analysis of Safety Properties -- A Policy Iteration Algorithm for Computing Fixed Points in Static Analysis of Programs -- Program Analysis and Verification II -- Data Structure Specifications via Local Equality Axioms -- Linear Ranking with Reachability -- Reasoning About Threads Communicating via Locks -- Applications of Learning -- Abstraction Refinement via Inductive Learning -- Automated Assume-Guarantee Reasoning for Simulation Conformance -- Symbolic Compositional Verification by Learning Assumptions

Control code

262680942

Dimensions

unknown

Extent

1 online resource (xv, 564 pages)

Form of item

online

Isbn

9783540316862

Media category

computer

Media MARC source

rdamedia

Media type code

• c

Other physical details

illustrations.

http://library.link/vocab/ext/overdrive/overdriveId

978-3-540-27231-1

Record ID

.b130042675

Specific material designation

remote

System control number

(OCoLC)262680942