@INPROCEEDINGS{BasinFriedrichGawkowski,
AUTHOR = "David Basin and Stefan Friedrich and Marek Gawkowski",
TITLE =  "Verified Bytecode Model Checkers",
BOOKTITLE = {Theorem Proving in Higher Order Logics (TPHOLs'02)},
YEAR = 2002,
PUBLISHER = "Springer-Verlag",
SERIES = "LNCS",
VOLUME = "2410",
ADDRESS = "Virginia, USA"
MONTH = "August",
PAGES = "47--66",
ABSTRACT =  {
We have used Isabelle/HOL to formalize and prove correct an approach to
bytecode verification based on model checking that we have developed for
the Java Virtual Machine.  Our work builds on, and extends, the
formalization of the Java Virtual Machine and data flow analysis
framework of Pusch and Nipkow.  By building on their framework, we can
reuse their results that relate the run-time behavior of programs with
the existence of well-typings for the programs.  Our primary extensions
are to handle polyvariant data flow analysis and its realization as
temporal logic model checking.  Aside from establishing the correctness
of our model-checking approach, our work contributes to understanding
the interrelationships between classical data flow analysis and program
analysis based on model checking.
}