| changeset 7691 | b7e8277fa088 |
| parent 7662 | 062a782d7402 |
| child 7983 | d823fdcc0645 |
--- 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.