Verification, Model Checking, and Abstract Interpretation : 10th International Conference, VMCAI 2009, Savannah, GA, USA, January 18-20, 2009. Proceedings / edited by Neil Jones, Markus Müller-Olm.

Format:

Book

Contributor:

Jones, Neil, editor.

Müller-Olm, Markus, editor.

SpringerLink (Online service)

Series:

Computer Science (Springer-11645)

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

Theoretical Computer Science and General Issues ; 5403

Language:

English

Subjects (All):

Computer programming.

Software engineering.

Programming languages (Electronic computers).

Computer logic.

Programming Techniques.

Software Engineering/Programming and Operating Systems.

Programming Languages, Compilers, Interpreters.

Logics and Meanings of Programs.

Software Engineering.

Local Subjects:

Programming Techniques.

Software Engineering/Programming and Operating Systems.

Programming Languages, Compilers, Interpreters.

Logics and Meanings of Programs.

Software Engineering.

Physical Description:

1 online resource (XI, 381 pages).

Edition:

First edition 2009.

Contained In:

Springer eBooks

Place of Publication:

Berlin, Heidelberg : Springer Berlin Heidelberg : Imprint: Springer, 2009.

System Details:

text file PDF

Summary:

The book constitutes the refereed proceedings of the 10th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2009, held in Savannah, GA, USA, in January 2009 - co-located with POPL 2009, the 36th Annual Symposium on Principles of Programming Languages. The 24 revised full papers presented together with 3 invited talks and 2 invited tutorials were carefully reviewed and selected from 72 submissions. The papers address all current issues from the communities of verification, model checking, and abstract interpretation, facilitating interaction, cross-fertilization, and advancement of hybrid methods that combine the three areas.

Contents:

Invited Talks

Model Checking: Progress and Problems

Model Checking Concurrent Programs

Thread-Modular Shape Analysis

Invited Tutorials

Advances in Program Termination and Liveness

Verification of Security Protocols

Submitted Papers

Towards Automatic Stability Analysis for Rely-Guarantee Proofs

Mostly-Functional Behavior in Java Programs

The Higher-Order Aggregate Update Problem

An Abort-Aware Model of Transactional Programming

Model-Checking the Linux Virtual File System

LTL Generalized Model Checking Revisited

Monitoring the Full Range of ?-Regular Properties of Stochastic Systems

Constraint-Based Invariant Inference over Predicate Abstraction

Reducing Behavioural to Structural Properties of Programs with Procedures

Query-Driven Program Testing

Average-Price-per-Reward Games on Hybrid Automata with Strong Resets

Abstraction Refinement for Probabilistic Software

Finding Concurrency-Related Bugs Using Random Isolation

An Abstract Interpretation-Based Framework for Control Flow Reconstruction from Binaries

SubPolyhedra: A (More) Scalable Approach to Infer Linear Inequalities

Deciding Extensions of the Theories of Vectors and Bags

A Posteriori Soundness for Non-deterministic Abstract Interpretations

An Automata-Theoretic Dynamic Completeness Criterion for Bounded Model-Checking

A Scalable Memory Model for Low-Level Code

Synthesizing Switching Logic Using Constraint Solving

Extending Symmetry Reduction by Exploiting System Architecture

Shape-Value Abstraction for Verifying Linearizability

Mixed Transition Systems Revisited

Counterexample Generation for Discrete-Time Markov Chains Using Bounded Model Checking.

Other Format:

Printed edition:

ISBN:

978-3-540-93900-9

9783540939009

Access Restriction:

Restricted for use by site license.