equal
deleted
inserted
replaced
26 |
26 |
27 <dt>BCV |
27 <dt>BCV |
28 <dd>generic model of bytecode verification, i.e. data-flow analysis |
28 <dd>generic model of bytecode verification, i.e. data-flow analysis |
29 for assembly languages with subtypes |
29 for assembly languages with subtypes |
30 |
30 |
31 <dt>HOL-Real |
31 <dt>HOL-Complex |
32 <dd>a development of the reals and hyper-reals, which are used in |
32 <dd>a development of the complex numbers, the reals, and the hyper-reals, |
33 non-standard analysis (builds the image HOL-Real) |
33 which are used in non-standard analysis (builds the image HOL-Complex) |
34 |
34 |
35 <dt>HOL-Real-HahnBanach |
35 <dt>HOL-Complex-HahnBanach |
36 <dd>the Hahn-Banach theorem for real vector spaces (in Isabelle/Isar) |
36 <dd>the Hahn-Banach theorem for real vector spaces (in Isabelle/Isar) |
37 |
37 |
38 <dt>HOL-Real-ex |
38 <dt>HOL-Complex-ex |
39 <dd>miscellaneous real number examples |
39 <dd>miscellaneous real ans complex number examples |
40 |
40 |
41 <dt>Hoare |
41 <dt>Hoare |
42 <dd>verification of imperative programs (verification conditions are |
42 <dd>verification of imperative programs (verification conditions are |
43 generated automatically from pre/post conditions and loop invariants) |
43 generated automatically from pre/post conditions and loop invariants) |
44 |
44 |