VMCAI 2004, Volume 5

Front Cover
Springer Science & Business Media, Jan 7, 2004 - Computers - 324 pages
This volume contains the proceedings of the 5th International Conference on Veri?cation, Model Checking, and Abstract Interpretation (VMCAI 2004), held inVenice, January11-13,2004, inconjunctionwithPOPL2004, the31stAnnual SymposiumonPrinciplesofProgrammingLanguages, January14-16,2004.The purposeofVMCAIistoprovideaforumforresearchersfromthreecommunities- veri?cation, model checking, and abstract interpretation-which will facilitate interaction, cross-fertilization, and the advance of hybrid methods that combine thethreeareas.Withthegrowingneedforformaltoolstoreasonaboutcomplex, in?nite-state, and embedded systems, such hybrid methods are bound to be of great importance. Topics covered by VMCAI include program veri?cation, static analysis te- niques, model checking, program certi?cation, type systems, abstract domains, debugging techniques, compiler optimization, embedded systems, and formal analysis of security protocols. This year's meeting follows the four previous events in Port Je?erson (1997), Pisa (1998), Venice (2002), LNCS 2294 and New York (2003), LNCS 2575. In particular, we thank VMCAI 2003's sponsor, the Courant Institute at New York University, for allowing us to apply a monetary surplus from the 2003 meeting to this one. The program committee selected 22 papers out of 68 on the basis of three - views.Theprincipalcriteriawererelevanceandquality.TheprogramofVMCAI 2004 included, in addition to the research papers, - a keynote speech by David Harel (Weizmann Institute, Israel) onAGrand Challenge for Computing: Full Reactive Modeling of a Multicellular Animal, - aninvitedtalkbyDawsonEngler(StanfordUniversity, USA)onStaticAn- ysis Versus Software Model Checking for Bug Finding, - an invited talk by Mooly Sagiv (Tel Aviv University, Israel) called On the Expressive Power of Canonical Abstraction, and -atutorialbyJoshuaD.Guttman(Mitre, USA)on Security, Protocols, and Trust. We would like to thank the Program Committee members and the reviewers, without whose dedicated e?ort the conference would not have been possible.
 

What people are saying - Write a review

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

Contents

Security Protocols and Trust
1
Security Types Preserving Compilation
2
HistoryDependent Scheduling for Cryptographic Processes
16
Construction of a Semantic Model for a Typed Assembly Language
30
RuleBased Runtime Verification
44
On the Expressive Power of Canonical Abstraction
58
Boolean Algebra of Shape Analysis Constraints
59
Approximate Probabilistic Model Checking
73
Certifying Temporal Properties for Compiled C Programs
161
Verifying Atomicity Specifications for Concurrent ObjectOriented Software Using ModelChecking
175
Static Analysis versus Software Model Checking for Bug Finding
191
Automatic Inference of Class Invariants
211
Liveness with Invisible Ranking
223
A Complete Method for the Synthesis of Linear Ranking Functions
239
Symbolic Implementation of the Best Transformer
252
Constructing Quantified Invariants via Predicate Abstraction
267

Completeness and Complexity of Bounded Model Checking
85
Model Checking for Object Specifications in Hidden Algebra
97
Model Checking Polygonal Differential Inclusions Using Invariance Kernels
110
Checking Interval Based Properties for Reactive Systems
122
Widening Operators for Powerset Domains
135
Type Inference for Parameterized RaceFree Java
149
Analysis of Recursive Game Graphs Using Data Flow Equations
282
Applying Jlint to Space Exploration Software
297
Why AI + ILP Is Good for WCET but MC Is Not Nor ILP Alone
309
Towards Full Reactive Modeling of a Multicellular Animal
323
Author Index
325
Copyright

Other editions - View all

Common terms and phrases