--- a/NEWS Mon Oct 04 14:45:35 1999 +0200
+++ b/NEWS Mon Oct 04 21:34:20 1999 +0200
@@ -170,6 +170,9 @@
* HOL/Real/HahnBanach: the Hahn-Banach theorem for real vector spaces
(in Isabelle/Isar) -- by Gertrud Bauer;
+* HOL/BCV: generic model of bytecode verification, i.e. data-flow
+analysis for assembly languages with subtypes;
+
* HOL/TLA (Lamport's Temporal Logic of Actions): major reorganization
-- avoids syntactic ambiguities and treats state, transition, and
temporal levels more uniformly; introduces INCOMPATIBILITIES due to
--- a/src/HOL/README.html Mon Oct 04 14:45:35 1999 +0200
+++ b/src/HOL/README.html Mon Oct 04 21:34:20 1999 +0200
@@ -29,6 +29,10 @@
</DL>
+<DT>BCV
+<DD>generic model of bytecode verification, i.e. data-flow analysis
+for assembly languages with subtypes.
+
<DT>Hoare
<DD>verification of imperative programs; verification conditions are
generated automatically from pre/post conditions and loop invariants.