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

Front Cover
Viktor Kuncak, Andrey Rybalchenko
Springer Science & Business Media, Jan 12, 2012 - Computers - 460 pages
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.
 

What people are saying - Write a review

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

Contents

Abstract Domains for Automated Reasoning about ListManipulating Programs with Infinite Data
1
Software Verification with Liquid Types
23
No More LSD Trip Proofs
24
An InterpolationBased Algorithm for Interprocedural Verification
39
Synchronizability for Verification of Asynchronously Communicating Systems
56
On the Termination of Integer Loops
72
Verification of GapOrder Constraint Abstractions of Counter Systems
88
On Application of MultiRooted Binary Decision Diagrams to Probabilistic Model Checking
104
Inferring Canonical Register Automata
251
Alternating Control Flow Reconstruction
267
Effective Synthesis of Asynchronous Systemsfrom GR1 Specifications
283
Sound Nonstatistical Clusteringof Static Analysis Alarms
299
Automating Induction with an SMT Solver
315
Modeling Asynchronous Message Passing for C Programs
332
Local Symmetry and Compositional Verification
348
A Verified Modern SAT Solver
363

Regression Verification for Multithreaded Programs
119
A Verifier for HigherOrder Store Programs
136
Synthesizing Protocols for Digital Contract Signing
152
Model Checking Information Flow in Reactive Systems
169
Splitting via Interpolants
186
Automatic Inference of Access Permissions
202
Lazy Synthesis
219
Efficient Nonconvex Domains for Abstract Interpretation
235
Decision Procedures for Region Logic
379
A General Framework for Probabilistic Characterizing Formulae
396
Loop Invariant Symbolic Execution for Parallel Programs
412
Synthesizing Efficient Controllers
428
Ideal Abstractions for WellStructured Transition Systems
445
Author Index
461
Copyright

Other editions - View all

Common terms and phrases

Bibliographic information