Research(Analysis last run in January 2008)2005--2007: 'encryption algorithms'; 'functional correctness proofs'; 'proof pearl'; 'termination analysis'; 'embedding cryptol'; 'elliptic curve cryptography'; 'ARM verification'; 'probabilistic guarded commands'; 'chess endgame data assurance';
2000--2004: 'theorem prover'; 'theorem proving'; 'higher order logic'; 'formal verification'; 'native code'; 'probabilistic algorithms'; 'probabilistic termination'; 'miller-rabin probabilistic primality test'; 'predicate sets'; 'logic variables'; 'HOL theorem prover'; 'polytypism in theorem proving'; 'formal approach'; 'compiling HOL4'; 'lcf-style interface'; 'first-order proof tactics'; 'formal semantics'; 'fast normalisation'; 'congruence classes';
| |
|