Computer Aided Verification : 12th International Conference, CAV 2000 Chicago, IL, USA, July 15-19, 2000 Proceedings / edited by E. Allen Emerson, A. Prasad Sistla.

Format:

Book

Contributor:

Emerson, E. Allen, editor.

Sistla, Aravinda Prasad, editor.

SpringerLink (Online service)

Series:

Computer Science (Springer-11645)

Lecture notes in computer science 0302-9743 ; 1855.

Lecture Notes in Computer Science, 0302-9743 ; 1855

Language:

English

Subjects (All):

Software engineering.

Computer logic.

Logic, Symbolic and mathematical.

Computers, Special purpose.

Artificial intelligence.

Software Engineering/Programming and Operating Systems.

Logics and Meanings of Programs.

Software Engineering.

Mathematical Logic and Formal Languages.

Special Purpose and Application-Based Systems.

Artificial Intelligence.

Local Subjects:

Software Engineering/Programming and Operating Systems.

Logics and Meanings of Programs.

Software Engineering.

Mathematical Logic and Formal Languages.

Special Purpose and Application-Based Systems.

Artificial Intelligence.

Physical Description:

1 online resource (X, 590 pages).

Edition:

First edition 2000.

Contained In:

Springer eBooks

Place of Publication:

Berlin, Heidelberg : Springer Berlin Heidelberg : Imprint: Springer, 2000.

System Details:

text file PDF

Summary:

This volume contains the proceedings of the 12th International Conference on Computer Aided Veri?cation (CAV 2000) held in Chicago, Illinois, USA during 15-19 July 2000. The CAV conferences are devoted to the advancement of the theory and practice of formal methods for hardware and software veri?cation. The con- rence covers the spectrum from theoretical foundations to concrete applications, with an emphasis on veri?cation algorithms, methods, and tools together with techniques for their implementation. The conference has traditionally drawn contributions from both researchers and practitioners in academia and industry. This year 91 regular research papers were submitted out of which 35 were - cepted, while 14 brief tool papers were submitted, out of which 9 were accepted for presentation. CAV included two invited talks and a panel discussion. CAV also included a tutorial day with two invited tutorials. Many industrial companies have shown a serious interest in CAV, ranging from using the presented technologies in their business to developing and m- keting their own formal veri?cation tools. We are very proud of the support we receive from industry. CAV 2000 was sponsored by a number of generous andforward-lookingcompaniesandorganizationsincluding:CadenceDesign- stems, IBM Research, Intel, Lucent Technologies, Mentor Graphics, the Minerva Center for Veri?cation of Reactive Systems, Siemens, and Synopsys. TheCAVconferencewasfoundedbyitsSteeringCommittee:EdmundClarke (CMU), Bob Kurshan (Bell Labs), Amir Pnueli (Weizmann), and Joseph Sifakis (Verimag).

Contents:

Invited Talks and Tutorials

Keynote Address: Abstraction, Composition, Symmetry, and a Little Deduction: The Remedies to State Explosion

Invited Address: Applying Formal Methods to Cryptographic Protocol Analysis

Invited Tutorial: Boolean Satisfiability Algorithms and Applications in Electronic Design Automation

Invited Tutorial: Verification of Infinite-state and Parameterized Systems

Regular Papers

An Abstraction Algorithm for the Verification of Generalized C-Slow Designs

Achieving Scalability in Parallel Reachability Analysis of Very Large Circuits

An Automata-Theoretic Approach to Reasoning about Infinite-State Systems

Automatic Verification of Parameterized Cache Coherence Protocols

Binary Reachability Analysis of Discrete Pushdown Timed Automata

Boolean Satisfiability with Transitivity Constraints

Bounded Model Construction for Monadic Second-Order Logics

Building Circuits from Relations

Combining Decision Diagrams and SAT Procedures for Efficient Symbolic Model Checking

On the Completeness of Compositional Reasoning

Counterexample-Guided Abstraction Refinement

Decision Procedures for Inductive Boolean Functions Based on Alternating Automata

Detecting Errors Before Reaching Them

A Discrete Strategy Improvement Algorithm for Solving Parity Games

Distributing Timed Model Checking - How the Search Order Matters

Efficient Algorithms for Model Checking Pushdown Systems

Efficient Büchi Automata from LTL Formulae

Efficient Detection of Global Properties in Distributed Systems Using Partial-Order Methods

Efficient Reachability Analysis of Hierarchical Reactive Machines

Formal Verification of VLIW Microprocessors with Speculative Execution

Induction in Compositional Model Checking

Liveness and Acceleration in Parameterized Verification

Mechanical Verification of an Ideal Incremental ABR Conformance Algorithm

Model Checking Continuous-Time Markov Chains by Transient Analysis

Model-Checking for Hybrid Systems by Quotienting and Constraints Solving

Prioritized Traversal: Efficient Reachability Analysis for Verification and Falsification

Regular Model Checking

Symbolic Techniques for Parametric Reasoning about Counter and Clock Systems

Syntactic Program Transformations for Automatic Abstraction

Temporal-logic Queries

Are Timed Automata Updatable?

Tuning SAT Checkers for Bounded Model Checking

Unfoldings of Unbounded Petri Nets

Verification Diagrams Revisited: Disjunctive Invariants for Easy Verification

Verifying Advanced Microarchitectures that Support Speculation and Exceptions

Tool Papers

FoCs - Automatic Generation of Simulation Checkers from Formal Specifications

IF: A Validation Environment for Timed Asynchronous Systems

Integrating WS1S with PVS

PET: An Interactive Software Testing Tool

A Proof-Carrying Code Architecture for Java

The Statemate Verification Environment

TAPS: A First-Order Verifier for Cryptographic Protocols

VINAS-P: A Tool for Trace Theoretic Verification of Timed Asynchronous Circuits

XMC: A Logic-Programming-Based Verification Toolset.

Other Format:

Printed edition:

ISBN:

978-3-540-45047-4

9783540450474

Access Restriction:

Restricted for use by site license.