E. Allen Emerson (auth.), Neil D. Jones, Markus Müller-Olm (eds.)3540938990, 9783540938996
The book constitutes the refereed proceedings of the 10th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2009, held in Savannah, GA, USA, in January 2009 – co-located with POPL 2009, the 36th Annual Symposium on Principles of Programming Languages.
The 24 revised full papers presented together with 3 invited talks and 2 invited tutorials were carefully reviewed and selected from 72 submissions. The papers address all current issues from the communities of verification, model checking, and abstract interpretation, facilitating interaction, cross-fertilization, and advancement of hybrid methods that combine the three areas.
Table of contents :
Front Matter….Pages –
Model Checking: Progress and Problems….Pages 1-1
Model Checking Concurrent Programs….Pages 2-2
Thread-Modular Shape Analysis….Pages 3-3
Advances in Program Termination and Liveness….Pages 4-4
Verification of Security Protocols….Pages 5-13
Towards Automatic Stability Analysis for Rely-Guarantee Proofs….Pages 14-28
Mostly-Functional Behavior in Java Programs….Pages 29-43
The Higher-Order Aggregate Update Problem….Pages 44-58
An Abort-Aware Model of Transactional Programming….Pages 59-73
Model-Checking the Linux Virtual File System….Pages 74-88
LTL Generalized Model Checking Revisited….Pages 89-104
Monitoring the Full Range of ω -Regular Properties of Stochastic Systems….Pages 105-119
Constraint-Based Invariant Inference over Predicate Abstraction….Pages 120-135
Reducing Behavioural to Structural Properties of Programs with Procedures….Pages 136-150
Query-Driven Program Testing….Pages 151-166
Average-Price-per-Reward Games on Hybrid Automata with Strong Resets….Pages 167-181
Abstraction Refinement for Probabilistic Software….Pages 182-197
Finding Concurrency-Related Bugs Using Random Isolation….Pages 198-213
An Abstract Interpretation-Based Framework for Control Flow Reconstruction from Binaries….Pages 214-228
SubPolyhedra: A (More) Scalable Approach to Infer Linear Inequalities….Pages 229-244
Deciding Extensions of the Theories of Vectors and Bags….Pages 245-259
A Posteriori Soundness for Non-deterministic Abstract Interpretations….Pages 260-274
An Automata-Theoretic Dynamic Completeness Criterion for Bounded Model-Checking….Pages 275-289
A Scalable Memory Model for Low-Level Code….Pages 290-304
Synthesizing Switching Logic Using Constraint Solving….Pages 305-319
Extending Symmetry Reduction by Exploiting System Architecture….Pages 320-334
Shape-Value Abstraction for Verifying Linearizability….Pages 335-348
Mixed Transition Systems Revisited….Pages 349-365
Counterexample Generation for Discrete-Time Markov Chains Using Bounded Model Checking….Pages 366-380
Back Matter….Pages –
Reviews
There are no reviews yet.