Verification, Model Checking, and Abstract Interpretation: 13th International Conference, VMCAI 2012, Philadelphia, PA, USA, January 22-24, 2012, Proceedings (Lecture Notes in Computer Science (7148))

This book constitutes the refereed proceedings of the 13th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2012, held in Philadelphia, PA, USA, in January 2012, co-located with the Symposium on Principles of Programming Languages, POPL 2012. The 26 revised full papers presented were carefully reviewed and selected from 70 submissions. The papers cover a wide range of topics including program verification, model checking, abstract interpretation, static analysis, deductive methods, program certification, debugging techniques, abstract domains, type systems, and optimization. Front Matter....Pages - Abstract Domains for Automated Reasoning about List-Manipulating Programs with Infinite Data....Pages 1-22 Software Verification with Liquid Types....Pages 23-23 Teaching Semantics with a Proof Assistant: No More LSD Trip Proofs....Pages 24-38 Whale : An Interpolation-Based Algorithm for Inter-procedural Verification....Pages 39-55 Synchronizability for Verification of Asynchronously Communicating Systems....Pages 56-71 On the Termination of Integer Loops....Pages 72-87 Verification of Gap-Order Constraint Abstractions of Counter Systems....Pages 88-103 On Application of Multi-Rooted Binary Decision Diagrams to Probabilistic Model Checking....Pages 104-118 Regression Verification for Multi-threaded Programs....Pages 119-135 Crowfoot: A Verifier for Higher-Order Store Programs....Pages 136-151 Synthesizing Protocols for Digital Contract Signing....Pages 152-168 Model Checking Information Flow in Reactive Systems....Pages 169-185 Splitting via Interpolants....Pages 186-201 Automatic Inference of Access Permissions....Pages 202-218 Lazy Synthesis....Pages 219-234 Donut Domains: Efficient Non-convex Domains for Abstract Interpretation....Pages 235-250 Inferring Canonical Register Automata....Pages 251-266 Alternating Control Flow Reconstruction....Pages 267-282 Effective Synthesis of Asynchronous Systems from GR(1) Specifications....Pages 283-298 Sound Non-statistical Clustering of Static Analysis Alarms....Pages 299-314 Automating Induction with an SMT Solver....Pages 315-331 Modeling Asynchronous Message Passing for C Programs....Pages 332-347 Local Symmetry and Compositional Verification....Pages 348-362 versat : A Verified Modern SAT Solver....Pages 363-378 Decision Procedures for Region Logic....Pages 379-395 A General Framework for Probabilistic Characterizing Formulae....Pages 396-411 Loop Invariant Symbolic Execution for Parallel Programs....Pages 412-427 Synthesizing Efficient Controllers....Pages 428-444 Ideal Abstractions for Well-Structured Transition Systems....Pages 445-460 Back Matter....Pages - This book constitutes the refereed proceedings of the 14th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2013, held in Rome, Italy, in January 2013, co-located with the Symposium on Principles of Programming Languages, POPL 2013.