Verification, Model Checking, and Abstract Interpretation: 13th International Conference, VMCAI 2012, Philadelphia, PA, USA, January 22-24, 2012, ProceedingsViktor Kuncak, Andrey Rybalchenko 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. |
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 |
Common terms and phrases
abstract domain abstract interpretation alarm clustering algorithm analysis assertion automatically automaton behavior binary decision diagrams bisimulation Boolean Büchi automaton compute constraints construct control flow counterexample Dafny defined definition denote edges encoding equivalence example execution formula function given heap Heidelberg Heidelberg 2010 Hoare triples implementation induction infinite input integer interpolants invariant iteration labeled language Lemma linear LNCS local symmetries logic loop loop invariants method model checking multiset nodes non-repudiation operator output over-approximation permission Petri nets postcondition predicate probabilistic problem procedure proof properties protocol prove PSPACE-complete queue quicksort reachable recursive refinement relation resp rule satisfies SecLTL Section semantics sequence SMT solver specification Springer static strategy symbolic synchronizable synchronous synthesis technique termination Theorem thread transition under-approximation valuation variables verification VMCAI