Verification, Model Checking, and Abstract Interpretation: 5th International Conference, VMCAI 2004 Venice, Italy, January 11-13, 2004 Proceedings

Joshua D. Guttman (auth.), Bernhard Steffen, Giorgio Levi (eds.)9783540208037, 9783540246220, 3540208038

This book constitutes the refereed proceedings of the 5th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2004, held in Venice, Italy in January 2004.

The 22 revised full papers presented together with 4 invited contributions were carefully reviewed and selected from 68 submissions. The papers are organized in topical sections on security, formal methods, model checking, software checking, liveness and completeness, and miscellaneous.

---

Table of contents :
Front Matter….Pages –
Security, Protocols, and Trust….Pages 1-1
Security Types Preserving Compilation….Pages 2-15
History-Dependent Scheduling for Cryptographic Processes….Pages 16-29
Construction of a Semantic Model for a Typed Assembly Language….Pages 30-43
Rule-Based Runtime Verification….Pages 44-57
On the Expressive Power of Canonical Abstraction….Pages 58-58
Boolean Algebra of Shape Analysis Constraints….Pages 59-72
Approximate Probabilistic Model Checking….Pages 73-84
Completeness and Complexity of Bounded Model Checking….Pages 85-96
Model Checking for Object Specifications in Hidden Algebra….Pages 97-109
Model Checking Polygonal Differential Inclusions Using Invariance Kernels….Pages 110-121
Checking Interval Based Properties for Reactive Systems….Pages 122-134
Widening Operators for Powerset Domains….Pages 135-148
Type Inference for Parameterized Race-Free Java….Pages 149-160
Certifying Temporal Properties for Compiled C Programs….Pages 161-174
Verifying Atomicity Specifications for Concurrent Object-Oriented Software Using Model-Checking….Pages 175-190
Static Analysis versus Software Model Checking for Bug Finding….Pages 191-210
Automatic Inference of Class Invariants….Pages 211-222
Liveness with Invisible Ranking….Pages 223-238
A Complete Method for the Synthesis of Linear Ranking Functions….Pages 239-251
Symbolic Implementation of the Best Transformer….Pages 252-266
Constructing Quantified Invariants via Predicate Abstraction….Pages 267-281
Analysis of Recursive Game Graphs Using Data Flow Equations….Pages 282-296
Applying Jlint to Space Exploration Software….Pages 297-308
Why AI + ILP Is Good for WCET, but MC Is Not, Nor ILP Alone….Pages 309-322
A Grand Challenge for Computing: Towards Full Reactive Modeling of a Multi-cellular Animal….Pages 323-324
Back Matter….Pages –