Verification, Model Checking, And Abstract Interpretation

by Emerson, E. Allen; Namjoshi, Kedar S.

• ISBN13: 9783540311393
• ISBN10: 3540311394
• Format: Paperback
• Copyright: 2006-02-15
• Publisher: Springer-Verlag New York Inc

Summary

The book constitutes the refereed proceedings of the 7th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2006, held in Charleston, South Carolina, USA in January 2006, co-located with the Symposium on Principles of Programming Languages (POPL 2006).The 27 revised full papers presented together with one invited paper were carefully reviewed and selected from 58 submissions. The papers feature current research from the communities of verification, model checking, and abstract interpretation, facilitating interaction, cross-fertilization, and advancement of hybrid methods.

Table of Contents

Closure operators for ROBDDs	p. 1
A CLP method for compositional and intermittent predicate abstraction	p. 17
Combining shape analyses by intersecting abstractions	p. 33
A complete abstract interpretation framework for coverability properties of WSTS	p. 49
Complexity results on branching-time pushdown model checking	p. 65
A compositional logic for control flow	p. 80
Detecting non-cyclicity by abstract compilation into Boolean functions	p. 95
Efficient strongly relational polyhedral analysis	p. 111
Environment abstraction for parameterized verification	p. 126
Error control for probabilistic model checking	p. 142
Field constraint analysis	p. 157
A framework for certified program analysis and its applications to mobile-code safety	p. 174
Improved algorithm complexities for linear temporal logic model checking of pushdown systems	p. 190
A logic and decision procedure for predicate abstraction of heap-manipulating programs	p. 207
Monitoring off-the-shelf components	p. 222
Parallel external directed model checking with linear I/O	p. 237
Piecewise FIFO channels are analyzable	p. 252
Ranking abstraction of recursive programs	p. 267
Relative safety	p. 282
Resource usage analysis for the [pi]-calculus	p. 298
Semantic hierarchy refactoring by abstract interpretation	p. 313
Strong preservation of temporal fixpoint-based operators by abstract interpretation	p. 332
Symbolic methods to enhance the precision of numerical abstract domains	p. 348
Synthesis of reactive(1) designs	p. 364
Systematic construction of abstractions for model-checking	p. 381
Totally clairvoyant scheduling with relative timing constraints	p. 398
Verification of well-formed communicating recursive state machines	p. 412
What's decidable about arrays?	p. 427
Table of Contents provided by Blackwell. All Rights Reserved.