--- a/src/HOL/MicroJava/document/root.bib Sun Mar 24 14:06:21 2002 +0100
+++ b/src/HOL/MicroJava/document/root.bib Sun Mar 24 19:16:51 2002 +0100
@@ -66,3 +66,28 @@
note = {ECOOP2000 Workshop proceedings available from \url{http://www.informatik.fernuni-hagen.de/pi5/publications.html}},
url = {\url{http://www4.in.tum.de/~nipkow/pubs/lbv.html}}
}
+
+
+@article{KleinN-CPE01,
+ author = "Gerwin Klein and Tobias Nipow",
+ title = "Verified Lightweight Bytecode Verification",
+ journal = "Concurrency and Computation: Practice and Experience",
+ year = "2001",
+ volume = "13",
+ number = "13",
+ editor = "Gary T. Leavens and Susan Eisenbach",
+ pages = "1133-1151",
+ url = {http://www4.informatik.tu-muenchen.de/~kleing/papers/cpe01.html},
+ abstract = {Eva and Kristoffer Rose proposed a (sparse) annotation of Java Virtual
+Machine code with types to enable a one-pass verification of welltypedness.
+We have formalized a variant of their proposal in the theorem prover
+Isabelle/HOL and proved soundness and completeness.},
+ note = {Invited contribution to special issue on Formal Techniques for Java},
+}
+
+
+@inproceedings{Nipkow-FOSSACS01,author={Tobias Nipkow},
+title={Verified Bytecode Verifiers},booktitle=
+{Foundations of Software Science and Computation Structures (FOSSACS 2001)},
+editor={F. Honsell},publisher=Springer,series=LNCS,volume=2030,
+pages={347--363},year=2001}