Verification, Model Checking, And Abstract Interpretation: 12th International Conference, Vmcai 2011, Austin, Tx, Usa, January 23-25, 2011 Proceedings (lecture Notes In Computer Science)

This book constitutes the refereed proceedings of the 12th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2011, held in Austin, TX, USA, in January 2011, co-located with the Symposium on Principles of Programming Languages, POPL 2011. The 24 revised full papers presented together with 4 invited talks were carefully reviewed and selected from 71 initial submissions. The papers showcases state-of-the-art research in areas such as verification, model checking, abstract interpretation and address any programming paradigm, including concurrent, constraint, functional, imperative, logic and object-oriented programming. Further topics covered are static analysis, deductive methods, program certification, debugging techniques, abstract domains, type systems, and optimization. Front Matter....Pages - Are Cells Asynchronous Circuits?....Pages 1-1 Formal Analysis of Message Passing....Pages 2-18 Practical Verification for the Working Programmer with CodeContracts and Abstract Interpretation....Pages 19-22 Quality Engineering: Leveraging Heterogeneous Information....Pages 23-37 More Precise Yet Widely Applicable Cost Analysis....Pages 38-53 Refinement-Based CFG Reconstruction from Unstructured Programs....Pages 54-69 SAT-Based Model Checking without Unrolling....Pages 70-87 Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic....Pages 88-102 Probabilistic Büchi Automata with Non-extremal Acceptance Thresholds....Pages 103-117 Synthesis of Fault-Tolerant Embedded Systems Using Games: From Theory to Practice....Pages 118-133 Proving Stabilization of Biological Systems....Pages 134-149 Precondition Inference from Intermittent Assertions and Application to Contracts on Collections....Pages 150-168 Strengthening Induction-Based Race Checking with Lightweight Static Analysis....Pages 169-183 Access Nets: Modeling Access to Physical Spaces....Pages 184-198 Join-Lock-Sensitive Forward Reachability Analysis for Concurrent Programs with Dynamic Process Creation....Pages 199-213 Verifying Deadlock-Freedom of Communication Fabrics....Pages 214-231 Static Analysis of Finite Precision Computations....Pages 232-247 An Evaluation of Automata Algorithms for String Analysis....Pages 248-262 Automata Learning with Automated Alphabet Abstraction Refinement....Pages 263-277 Towards Complete Reasoning about Axiomatic Specifications....Pages 278-293 String Analysis as an Abstract Interpretation....Pages 294-308 ExplainHoudini: Making Houdini Inference Transparent....Pages 309-323 Abstract Probabilistic Automata....Pages 324-339 Distributed and Predictable Software Model Checking....Pages 340-355 Access Analysis-Based Tight Localization of Abstract Memories....Pages 356-370 Decision Procedures for Automating Termination Proofs....Pages 371-386 Collective Assertions....Pages 387-402 Sets with Cardinality Constraints in Satisfiability Modulo Theories....Pages 403-418 Back Matter....Pages -