added BVC;
authorwenzelm
Mon Oct 04 21:34:20 1999 +0200 (1999-10-04)
changeset 7691b7e8277fa088
parent 7690 27676b51243d
child 7692 89bbce6f5c17
added BVC;
NEWS
src/HOL/README.html
     1.1 --- a/NEWS	Mon Oct 04 14:45:35 1999 +0200
     1.2 +++ b/NEWS	Mon Oct 04 21:34:20 1999 +0200
     1.3 @@ -170,6 +170,9 @@
     1.4  * HOL/Real/HahnBanach: the Hahn-Banach theorem for real vector spaces
     1.5  (in Isabelle/Isar) -- by Gertrud Bauer;
     1.6  
     1.7 +* HOL/BCV: generic model of bytecode verification, i.e. data-flow
     1.8 +analysis for assembly languages with subtypes;
     1.9 +
    1.10  * HOL/TLA (Lamport's Temporal Logic of Actions): major reorganization
    1.11  -- avoids syntactic ambiguities and treats state, transition, and
    1.12  temporal levels more uniformly; introduces INCOMPATIBILITIES due to
     2.1 --- a/src/HOL/README.html	Mon Oct 04 14:45:35 1999 +0200
     2.2 +++ b/src/HOL/README.html	Mon Oct 04 21:34:20 1999 +0200
     2.3 @@ -29,6 +29,10 @@
     2.4  
     2.5  </DL>
     2.6  
     2.7 +<DT>BCV
     2.8 +<DD>generic model of bytecode verification, i.e. data-flow analysis
     2.9 +for assembly languages with subtypes.
    2.10 +
    2.11  <DT>Hoare
    2.12  <DD>verification of imperative programs; verification conditions are
    2.13  generated automatically from pre/post conditions and loop invariants.