Computer Aided Verification : 17th International Conference, CAV 2005, Edinburgh, Scotland, UK, July 6-10, 2005, Proceedings / edited by Kousha Etessami, Sriram K. Rajamani.

Format:

Book

Contributor:

Etessami, Kousha, editor.

Rajamani, Sriram K., 1970- editor.

SpringerLink (Online service)

Series:

Computer Science (Springer-11645)

LNCS sublibrary. Theoretical computer science and general issues ; SL 1, 3576.

Theoretical Computer Science and General Issues ; 3576

Language:

English

Subjects (All):

Computer logic.

Software engineering.

Logic, Symbolic and mathematical.

Artificial intelligence.

Logic design.

Logics and Meanings of Programs.

Software Engineering.

Mathematical Logic and Formal Languages.

Artificial Intelligence.

Logic Design.

Local Subjects:

Logics and Meanings of Programs.

Software Engineering.

Mathematical Logic and Formal Languages.

Artificial Intelligence.

Logic Design.

Physical Description:

1 online resource (XVI, 568 pages).

Edition:

First edition 2005.

Contained In:

Springer eBooks

Place of Publication:

Berlin, Heidelberg : Springer Berlin Heidelberg : Imprint: Springer, 2005.

System Details:

text file PDF

Summary:

This volume contains the proceedings of the International Conference on Computer Aided Veri?cation (CAV), held in Edinburgh, Scotland, July 6-10, 2005. CAV 2005 was the seventeenth in a series of conferences dedicated to the advancement of the theory and practice of computer-assisted formal an- ysis methods for software and hardware systems. The conference covered the spectrum from theoretical results to concrete applications, with an emphasis on practical veri?cation tools and the algorithms and techniques that are needed for their implementation. We received 123 submissions for regular papers and 32 submissions for tool papers.Ofthesesubmissions,theProgramCommitteeselected32regularpapers and 16 tool papers, which formed the technical program of the conference. The conference had three invited talks, by Bob Bentley (Intel), Bud Mishra (NYU), and George C. Necula (UC Berkeley). The conference was preceded by a tutorial day, with two tutorials: - Automated Abstraction Re?nement, by Thomas Ball (Microsoft) and Ken McMillan (Cadence); and - Theory and Practice of Decision Procedures for Combinations of (First- Order) Theories, by Clark Barrett (NYU) and Cesare Tinelli (U Iowa). CAV 2005 had six a?liated workshops: - BMC 2005: 3rd Int. Workshop on Bounded Model Checking; - FATES 2005: 5th Workshop on Formal Approaches to Testing Software; - GDV 2005: 2nd Workshop on Games in Design and Veri?cation; - PDPAR 2005: 3rd Workshop on Pragmatics of Decision Procedures in - tomated Reasoning; - RV 2005: 5th Workshop on Runtime Veri?cation; and - SoftMC 2005: 3rd Workshop on Software Model Checking.

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.

Other Format:

Printed edition:

ISBN:

978-3-540-31686-2

9783540316862

Access Restriction:

Restricted for use by site license.