src/HOL/README.html
changeset 7691 b7e8277fa088
parent 7662 062a782d7402
child 7983 d823fdcc0645
     1.1 --- a/src/HOL/README.html	Mon Oct 04 14:45:35 1999 +0200
     1.2 +++ b/src/HOL/README.html	Mon Oct 04 21:34:20 1999 +0200
     1.3 @@ -29,6 +29,10 @@
     1.4  
     1.5  </DL>
     1.6  
     1.7 +<DT>BCV
     1.8 +<DD>generic model of bytecode verification, i.e. data-flow analysis
     1.9 +for assembly languages with subtypes.
    1.10 +
    1.11  <DT>Hoare
    1.12  <DD>verification of imperative programs; verification conditions are
    1.13  generated automatically from pre/post conditions and loop invariants.