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

---

Marc Notes: post-proceedings (consisting of thoroughly revised final full papers);research monographs (which may be based on outstanding PhD work, research projects, technical reports, etc.); More recently, several color-cover sublines have been added featuring, beyond a collection of papers, various added-value component;these sublines include;tutorials (textbook-like monographs or collections of lectures given at advanced courses);state-of-the-art surveys (offering complete and mediated coverage of a topic);hot topics (introducing emergent topics to the broader community); In parallel to the printed book, each new volume is published electronic in LNCS Online.; The scope of LNCS, including its subseries LNAI and LNBI, spans the whole range of computer science and information technology including interdisciplinary topics in a variety of application fields. The type of material published traditionally includes;proceedings (published in time for the respective conference); The LNCS series reports state-of-the-art results in computer science research, development, and education, at a high level and in both printed and electronic form. Enjoying tight cooperation with the R&D community, with numerous individuals, as well as with prestigious organizations and societies, LNCS has grown into the most comprehensive computer science research forum available. Table of Contents: Abstract Domains for Automated Reasoning about List-Manipulating Programs with Infinite Data / Ahmed Bouajjani, Cezara Dragoi, Constantin Enea, Mihaela Sighireanu -- Software Verification with Liquid Types (Abstract) / Ranjit Jhala -- Teaching Semantics with a Proof Assistant: No More LSD Trip Proofs / Tobias Nipkow -- WHALE: An Interpolation-Based Algorithm for Inter-procedural Verification / Aws Albarghouthi, Arie Gurfinkel, Marsha Chechik -- Synchronizability for Verification of Asynchronously Communicating Systems / Samik Basu, Tevfik Bultan, Meriem Ouederni -- On the Termination of Integer Loops / Amir M. Ben-Amram, Samir Genaim, Abu Naser Masud -- Verification of Gap-Order Constraint Abstractions of Counter Systems / Laura Bozzelli, Sophie Pinchinat -- On Application of Multi-Rooted Binary Decision Diagrams to Probabilistic Model Checking / Dmitry Bugaychenko -- Regression Verification for Multi-threaded Programs / Sagar Chaki, Arie Gurfinkel, Ofer Strichman -- Crowfoot: A Verifier for Higher-Order Store Programs / Nathaniel Charlton, Ben Horsfall, Bernhard Reus -- Synthesizing Protocols for Digital Contract Signing / Krishnendu Chatterjee, Vishwanath Raman -- Model Checking Information Flow in Reactive Systems / Rayna Dimitrova, Bernd Finkbeiner, Mate Kovacs, Markus N. Rabe, Helmut Seidl -- Splitting via Interpolants / Evren Ermis, Jochen Hoenicke, Andreas Podelski -- Automatic Inference of Access Permissions / Pietro Ferrara, Peter Muller -- Lazy Synthesis / Bernd Finkbeiner, Swen Jacobs -- Donut Domains: Efficient Non-convex Domains for Abstract Interpretation / Khalil Ghorbal, Franjo Ivancic, Gogul Balakrishnan, Naoto Maeda, Aarti Gupta -- Inferring Canonical Register Automata / Falk Howar, Bernhard Steffen, Bengt Jonsson, Sofia Cassel -- Alternating Control Flow Reconstruction / Johannes Kinder, Dmitry Kravchenko -- Effective Synthesis of Asynchronous Systems from GR(1) Specifications / Uri Klein, Nir Piterman, Amir Pnueli -- Sound Non-statistical Clustering of Static Analysis Alarms / Woosuk Lee, Wonchan Lee, Kwangkeun Yi -- Automating Induction with an SMT Solver / K. Rustan M. Leino -- Modeling Asynchronous Message Passing for C Programs / Everett Morse, Nick Vrvilo, Eric Mercer, Jay McCarthy -- Local Symmetry and Compositional Verification / Kedar S. Namjoshi, Richard J. Trefler -- versat: A Verified Modern SAT Solver / Duckki Oe, Aaron Stump, Corey Oliver, Kevin Clancy -- Decision Procedures for Region Logic / Stan Rosenberg, Anindya Banerjee, David A. Naumann -- A General Framework for Probabilistic Characterizing Formulae / Joshua Sack, Lijun Zhang -- Loop Invariant Symbolic Execution for Parallel Programs / Stephen F. Siegel, Timothy K. Zirkel -- Synthesizing Efficient Controllers / Christian von Essen, Barbara Jobstmann -- Ideal Abstractions for Well-Structured Transition Systems / Damien Zufferey, Thomas Wies, Thomas A. Henzinger -- Author Index. Publisher Marketing: 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.