src/HOL/BCV/README.html
author wenzelm
Mon, 03 Apr 2000 14:02:40 +0200
changeset 8662 f9679ddbc492
parent 7626 5997f35954d7
child 9791 a39e5d43de55
permissions -rw-r--r--
isapar, isamarkuptext, isamarkuptxt turned into environments;

<HTML><HEAD><TITLE>HOL/BCV/README</TITLE></HEAD>
<BODY>

<H1>Towards 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.

<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>.

</BODY>
</HTML>