# HG changeset patch
# User wenzelm
# Date 939065660 -7200
# Node ID b7e8277fa088110b0699860ba3fa5b0384e7129a
# Parent  27676b51243d65760f54ff1e396fefdb4ee09e66
added BVC;

diff -r 27676b51243d -r b7e8277fa088 NEWS
--- 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
diff -r 27676b51243d -r b7e8277fa088 src/HOL/README.html
--- 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.