Description
Springer Verification Model Checking And Abstract Interpretation2009 Edition by Neil Jones Markus Müller-Olm
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?erson1997Pisa1998Venice2002NewYork2003Venice2004 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". 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.