|
7626
|
1 |
<HTML><HEAD><TITLE>HOL/BCV/README</TITLE></HEAD>
|
|
|
2 |
<BODY>
|
|
|
3 |
|
|
9791
|
4 |
<H1>Verified Bytecode Verifiers</H1>
|
|
7626
|
5 |
|
|
9791
|
6 |
This theory defines an abstract and generic model of bytecode
|
|
|
7 |
verification, i.e. data-flow analysis for assembly languages with subtypes,
|
|
|
8 |
and applies it to an equally abstract model of the JVM.
|
|
7626
|
9 |
|
|
|
10 |
<P>
|
|
|
11 |
|
|
|
12 |
A paper describing the theory is found here:
|
|
9791
|
13 |
<A HREF = "http://www.in.tum.de/~nipkow/pubs/bcv2.html">
|
|
|
14 |
Verified Bytecode Verifiers</A>.
|
|
7626
|
15 |
|
|
|
16 |
</BODY>
|
|
|
17 |
</HTML>
|