Verification, Model Checking, and Abstract Interpretation: 12th International Conference, VMCAI 2011, Austin, TX, USA, January 23-25, 2011 Proceedings

Front Cover
Ranjit Jhala, David Schmidt
Springer Science & Business Media, Jan 11, 2011 - Computers - 419 pages
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.
 

What people are saying - Write a review

We haven't found any reviews in the usual places.

Contents

Are Cells Asynchronous Circuits? Invited Talk
1
Formal Analysis of Message Passing Invited Talk
2
Practical Verification for the Working Programmer with CodeContracts and Abstract Interpretation Invited Talk
19
Leveraging Heterogeneous Information Invited Talk
23
More Precise Yet Widely Applicable Cost Analysis
38
RefinementBased CFG Reconstruction from Unstructured Programs
54
SATBased Model Checking without Unrolling
70
Beyond QuantifierFree Interpolation in Extensions of Presburger Arithmetic
88
Verifying DeadlockFreedom of Communication Fabrics
214
Static Analysis of Finite Precision Computations
232
An Evaluation of Automata Algorithms for String Analysis
248
Automata Learning with Automated Alphabet Abstraction Refinement
263
Towards Complete Reasoning about Axiomatic Specifications
278
String Analysis as an Abstract Interpretation
294
Making Houdini Inference Transparent
309
Abstract Probabilistic Automata
324

Probabilistic Buchi Automata with Nonextremal Acceptance Thresholds
103
From Theory to Practice
118
Proving Stabilization of Biological Systems
134
Precondition Inference from Intermittent Assertions and Application to Contracts on Collections
150
Strengthening InductionBased Race Checking with Lightweight Static Analysis
169
Modeling Access to Physical Spaces
184
JoinLockSensitive Forward Reachability Analysis for Concurrent Programs with Dynamic Process Creation
199
Distributed and Predictable Software Model Checking
340
Access AnalysisBased Tight Localization of Abstract Memories
356
Decision Procedures for Automating Termination Proofs
371
Collective Assertions
387
Sets with Cardinality Constraints in Satisfiability Modulo Theories
403
Author Index
419
Copyright

Other editions - View all

Common terms and phrases

Bibliographic information