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.
