Disclaimer: All content has been generated automatically by a program running on the titles of publications extracted from people's webpages. Click here for details. ©2007 Advaith Siddharthan
 
Mike Gordon
 

Research

(Analysis last run in January 2008)

2005--2007: 'higher order logic'; 'automated reasoning'; 'ARM machine code'; 'psl/sugar semantics'; 'peer-to-peer overlays'; 'automatic formal synthesis'; 'elliptic curve cryptography'; 'ARM verification'; 'modelsled machine code'; 'proof-producing hardware compiler';

2000--2004: 'hardware description languages'; 'trace semantics'; 'bdd-based symbolic calculation'; 'theorem proving'; 'HOL4 theorem'; 'formal semantics';

Related People
  • Joe Hurd [ ARG ]:
    • 'ARM verification'; 'HOL theorem prover'; 'elliptic curve cryptography'; 'formal approach'; 'higher order logic'; 'theorem proving';
  • Anthony Fox [ ARG ]:
    • 'ARM machine code'; 'ARM verification'; 'HOL specification'; 'elliptic curve cryptography'; 'formal specification';
  • Larry Paulson [ Security ][ TSG ][ ARG ]:
    • 'compositional reasoning'; 'formal verification'; 'interactive theorem proving'; 'reflection theorem';
  • Mateja Jamnik [ AI ][ ARG ]:
    • 'diagrammatic reasoning'; 'systems description'; 'theorem proving';
  • Magnus Myreen [ ARG ]:
    • 'ARM machine code'; 'modelsled machine code';
  • Matthew Parkinson [ TSG ]:
    • 'local reasoning'; 'modular verification'; 'semantic definition';
  • David Greaves [ CAG ]:
    • 'formal specification'; 'hardware specifications';
 

Disclaimer: All content has been generated automatically by a program running on the titles of publications extracted from people's webpages.
©2007 Advaith Siddharthan, Computer Laboratory, University of Cambridge. Please send any comments on this page to as372@cl.cam.ac.uk