Overview

This volume contains the proceedings of the 10th International Conference on Veri?cation, Model Checking, and Abstract Interpretation (VMCAI 2009), held in Savannah, Georgia, USA, January 18–20, 2009. VMCAI 2009 was the 10th in a series of meetings. Previous meetings were heldinPortJe?erson1997,Pisa1998,Venice2002,NewYork2003,Venice2004, Paris 2005, Charleston 2006, Nice 2007, and San Francisco 2008. VMCAI centers on state-of-the-art research relevant to analysis of programs and systems and drawn from three research communities: veri?cation, model checking, and abstract interpretation. A goal is to facilitate interaction, cro- fertilization, and the advance of hybrid methods that combine two or all three areas. Topics covered by VMCAI include program veri?cation, program cert- cation, model checking, debugging techniques, abstract interpretation, abstract domains, static analysis, type systems, deductive methods, and optimization. The Program Committee selected 24 papers out of 72 submissions based on anonymous reviews and discussions in an electronic Program Committee me- ing. The principal selection criteria were relevance and quality. VMCAI has a tradition of inviting distinguished speakers to give talks and tutorials. This time the program included three invited talks by: – E. Allen Emerson (University of Texas at Austin) on “Model Checking: Progress and Problems” – Aarti Gupta (NEC Labs, Princeton) on “Model Checking Concurrent Programs” – Mooly Sagiv (Tel-Aviv University) on “Thread Modular Shape Analysis” There were also two invited tutorials by: – Byron Cook (Microsoft Research, Cambridge) on “Proving Program Ter- nation and Liveness” – V´ eroniqueCortier (LORIA, CNRS, Nancy) on“Veri?cationof Security P- tocols”.

Full Product Details

Author:   Neil Jones ,  Markus Müller-Olm
Publisher:   Springer-Verlag Berlin and Heidelberg GmbH & Co. KG
Imprint:   Springer-Verlag Berlin and Heidelberg GmbH & Co. K
Edition:   2008 ed.
Volume:   5403
Dimensions:   Width: 15.50cm , Height: 2.00cm , Length: 23.50cm
Weight:   0.605kg
ISBN:  

9783540938996

ISBN 10:   3540938990
Pages:   381
Publication Date:   18 December 2008
Audience:   Professional and scholarly ,  Professional & Vocational
Format:   Paperback
Publisher's Status:   Active
Availability:   In Print  
This item will be ordered in for you from one of our suppliers. Upon receipt, we will promptly dispatch it out to you. For in store availability, please contact us.

Table of 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.

Reviews

Author Information

Tab Content 6

Author Website:  

Customer Reviews

Recent Reviews

No review item found!

Add your own review!

Countries Available

All regions