| author | wenzelm |
| Fri, 06 Oct 2000 17:35:58 +0200 | |
| changeset 10168 | 50be659d4222 |
| parent 9791 | a39e5d43de55 |
| permissions | -rw-r--r-- |
<HTML><HEAD><TITLE>HOL/BCV/README</TITLE></HEAD> <BODY> <H1>Verified Bytecode Verifiers</H1> 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://www.in.tum.de/~nipkow/pubs/bcv2.html"> Verified Bytecode Verifiers</A>. </BODY> </HTML>