src/HOL/BCV/README.html
changeset 9791 a39e5d43de55
parent 7626 5997f35954d7
--- a/src/HOL/BCV/README.html	Fri Sep 01 18:01:05 2000 +0200
+++ b/src/HOL/BCV/README.html	Fri Sep 01 18:29:52 2000 +0200
@@ -1,16 +1,17 @@
 <HTML><HEAD><TITLE>HOL/BCV/README</TITLE></HEAD>
 <BODY>
 
-<H1>Towards Verified Bytecode Verifiers</H1>
+<H1>Verified Bytecode Verifiers</H1>
 
-This theory defines a very abstract and generic model of bytecode
-verification, i.e. data-flow analysis for assembly languages with subtypes.
+This theory defines an abstract and generic model of bytecode
+verification, i.e. data-flow analysis for assembly languages with subtypes,
+and applies it to an equally abstract model of the JVM.
 
 <P>
 
 A paper describing the theory is found here:
-<A HREF = "http://www4.in.tum.de/~nipkow/pubs/bcv.html">
-Towards Verified Bytecode Verifiers</A>.
+<A HREF = "http://www.in.tum.de/~nipkow/pubs/bcv2.html">
+Verified Bytecode Verifiers</A>.
 
 </BODY>
 </HTML>