Verification, Model Checking, and Abstract Interpretation : 6th International Conference, VMCAI 2005, Paris, France, January 17-19, 2005, Proceedings / edited by Radhia Cousot.

Format:

Book

Conference/Event

Contributor:

Cousot, Radhia.

Conference Name:

VMCAI 2005 (2005 : Paris, France)

Series:

Theoretical Computer Science and General Issues, 2512-2029 ; 3385

Language:

English

Subjects (All):

Software engineering.

Computer science.

Compilers (Computer programs).

Software Engineering.

Computer Science Logic and Foundations of Programming.

Compilers and Interpreters.

Local Subjects:

Software Engineering.

Computer Science Logic and Foundations of Programming.

Compilers and Interpreters.

Physical Description:

1 online resource (XII, 483 p.)

Edition:

1st ed. 2005.

Place of Publication:

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

Language Note:

English

Summary:

This volume contains the papers accepted for presentation at the 6th Inter- tional Conference on Veri'cation, Model Checking and Abstract Interpretation (VMCAI 2005), which was held January 17-19, 2005 in Paris, France. VMCAI provides a forum for researchers from the communities of veri?- tion, model checking, and abstract interpretation, facilitating interaction, cro- fertilization, and advancement of hybrid methods that combine the three areas. With the growing need for formal methods to reason about complex, in'ni- state, and embedded systems, such hybrid methods are bound to be of great importance. VMCAI 2005 received 92 submissions. Each paper was carefully reviewed, being judged according to scienti'c quality, originality, and relevance to the symposium topics. Following online discussions, the program committee met in ´ Paris,France,attheEcoleNormaleSup´ erieureonOctober30,2004,andselected 27 papers. In addition to the contributed papers, this volume includes contributions by outstanding invited speakers: ´ - Patrick Cousot (Ecole Normale Sup´ erieure, Paris), Proving Program Inva- ance and Termination by Parametric Abstraction, Lagrangian Relaxation and Semide'nite Programming; - C.A.R. Hoare (Microsoft Research, Cambridge), The Verifying Compiler, a Grand Challenge for Computing Research; - Amir Pnueli (New York University and Weizmann Institute of Science), - straction for Liveness. The VMCAI 2005 program included an invited tutorial by Sriram K. Ra- mani (Microsoft Research,Redmond) on Model Checking, Abstraction and S- bolic Execution for Software. VMCAI 2005 was followed by workshops on Automatic Tools for Veri?- tion, Abstract Interpretation of Object-Oriented Languages, and Numerical & Symbolic Abstract Domains.

Contents:

Invited Paper

Proving Program Invariance and Termination by Parametric Abstraction, Lagrangian Relaxation and Semidefinite Programming

Numerical Abstraction

Scalable Analysis of Linear Systems Using Mathematical Programming

The Arithmetic-Geometric Progression Abstract Domain

An Overview of Semantics for the Validation of Numerical Programs

Invited Talk

The Verifying Compiler, a Grand Challenge for Computing Research

Verification I

Checking Herbrand Equalities and Beyond

Static Analysis by Abstract Interpretation of the Quasi-synchronous Composition of Synchronous Programs

Termination of Polynomial Programs

Verifying Safety of a Token Coherence Implementation by Parametric Compositional Refinement

Abstraction for Liveness

Heap and Shape Analysis

Abstract Interpretation with Alien Expressions and Heap Structures

Shape Analysis by Predicate Abstraction

Predicate Abstraction and Canonical Abstraction for Singly-Linked Lists

Purity and Side Effect Analysis for Java Programs

Abstract Model Checking

Automata as Abstractions

Don’t Know in the ?-Calculus

Model Checking of Systems Employing Commutative Functions

Model Checking

Weak Automata for the Linear Time ?-Calculus

Model Checking for Process Rewrite Systems and a Class of Action-Based Regular Properties

Minimizing Counterexample with Unit Core Extraction and Incremental SAT

I/O Efficient Directed Model Checking

Applied Abstract Interpretation

Verification of an Error Correcting Code by Abstract Interpretation

Information Flow Analysis for Java Bytecode

Cryptographic Protocol Analysis on Real C Code

Bounded Model Checking

Simple Is Better: Efficient Bounded Model Checking for Past LTL

Optimizing Bounded Model Checking for Linear HybridSystems

Verification II

Efficient Verification of Halting Properties for MPI Programs with Wildcard Receives

Generalized Typestate Checking for Data Structure Consistency

On the Complexity of Error Explanation

Efficiently Verifiable Conditions for Deadlock-Freedom of Large Concurrent Programs.

Notes:

Bibliographic Level Mode of Issuance: Monograph

Includes bibliographical references and index.

ISBN:

3-540-30579-3