+612 9045 4394
Verification, Model Checking, and Abstract Interpretation : 5th International Conference, Vmcai 2004, Venice, January 11-13, 2004, Proceedings - Bernhard Steffen

Verification, Model Checking, and Abstract Interpretation

5th International Conference, Vmcai 2004, Venice, January 11-13, 2004, Proceedings

By: Bernhard Steffen (Editor), Giorgio Levi (Editor)

Paperback Published: 7th January 2004
ISBN: 9783540208037
Number Of Pages: 325

Share This Book:


or 4 easy payments of $33.88 with Learn more
Ships in 7 to 10 business days

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.

Security, Protocols, and Trustp. 1
Security Types Preserving Compilationp. 2
History-Dependent Scheduling for Cryptographic Processesp. 16
Construction of a Semantic Model for a Typed Assembly Languagep. 30
Rule-Based Runtime Verificationp. 44
On the Expressive Power of Canonical Abstractionp. 58
Boolean Algebra of Shape Analysis Constraintsp. 59
Approximate Probabilistic Model Checkingp. 73
Completeness and Complexity of Bounded Model Checkingp. 85
Model Checking for Object Specifications in Hidden Algebrap. 97
Model Checking Polygonal Differential Inclusions Using Invariance Kernelsp. 110
Checking Interval Based Properties for Reactive Systemsp. 122
Widening Operators for Powerset Domainsp. 135
Type Inference for Parameterized Race-Free Javap. 149
Certifying Temporal Properties for Compiled C Programsp. 161
Verifying Atomicity Specifications for Concurrent Object-Oriented Software Using Model-Checkingp. 175
Static Analysis versus Software Model Checking for Bug Findingp. 191
Automatic Inference of Class Invariantsp. 211
Liveness with Invisible Rankingp. 223
A Complete Method for the Synthesis of Linear Ranking Functionsp. 239
Symbolic Implementation of the Best Transformerp. 252
Constructing Quantified Invariants via Predicate Abstractionp. 267
Analysis of Recursive Game Graphs Using Data Flow Equationsp. 282
Applying Jlint to Space Exploration Softwarep. 297
Why AI + ILP Is Good for WCET, but MC Is Not, Nor ILP Alonep. 309
A Grand Challenge for Computing: Towards Full Reactive Modeling of a Multi-cellular Animalp. 323
Author Indexp. 325
Table of Contents provided by Blackwell. All Rights Reserved.

ISBN: 9783540208037
ISBN-10: 3540208038
Series: Lecture Notes in Computer Science,
Audience: General
Format: Paperback
Language: English
Number Of Pages: 325
Published: 7th January 2004
Publisher: Springer-Verlag Berlin and Heidelberg Gmbh & Co. Kg
Country of Publication: US
Dimensions (cm): 23.39 x 15.6  x 1.83
Weight (kg): 0.48