EPSRC logo
Researcher Details
 
Name: Professor M Gordon
Organisation: University of Cambridge
Department: Computer Science and Technology
Current EPSRC-Supported Research Topics:
Fundamentals of Computing

Current EPSRC Support
EP/K008528/1 REMS: Rigorous Engineering for Mainstream Systems(C)
Previous EPSRC Support
EP/H010815/1 jStar: making java verification practical(P)
EP/F067909/1 Expressive Multi-theory Reasoning for Interactive Verification(P)
EP/G007411/1 Trustworthy programming for multiple instruction sets(P)
GR/T06315/01 Applications of Theorem Proving to Assertion Based Verification(P)
GR/T20106/01 Formal Specification and Verification of ARM-Based Systems(P)
GR/R27105/01 Fully Expansive Proof and Algorithmic Verification(P)
GR/R07615/01 Freshml: a Fresh Approach To Name Binding In Metaprogramming Languages(C)
GR/N13135/01 FORMAL SPECIFICATION AND VERIFICATION OF ARM6(P)
GR/L74262/01 A UNIFORM SEMANTICS FOR VERILOG AND VHDL SUITABLE FOR BOTH SIMULATION AND FORMAL VERIFICATION(C)
GR/L35980/01 A HARDWARE COMPILATION WORKBENCH(P)
GR/L03071/01 AUTOMATIC GUIDENCE OF MECHANICALLY GENERATED PROOFS(P)
GR/K58395/01 FLOATING - POINT VERIFICATION(P)
GR/K57381/01 MECHANISING TEMPORAL REASONING(C)
GR/K57343/01 CHECKING EQUIVALENCE BETWEEN SYNTHESISED LOGIC AND NON-SYNTHESISABLE BEHAVIOURAL PROTOTYPES(C)
GR/K10294/01 HIERARCHICAL FORMAL VERIFICATION OF COMMUNICATION NETWORKS(P)
GR/J42236/01 A SEMANTICALLY BASED DESIGN ENVIRONMENT FOR ASICS(P)
GR/J11133/01 FORMAL VERIFICATIONS OF ASPECTS OF AN ASYNCHRONOUS TRANSFER MODE NETWORK.(P)
GR/H40570/01 COMBINING HOL WITH ISABELLE(C)
GR/G23654/01 REPRESENTATION AND VALIDATION OF MECHANICALLY GENERATED PROOFS(P)
GR/G33837/01 HOL VERIFICATION OF ELLA DESIGNS(P)
GR/F36675/01 FOUNDATIONS AND TOOLS FOR FORMAL VERIFICATION(P)
GR/F36484/01 DEMONSTRATION OF THE POSSIBILITY OF TOTALLY VERIFIED SYSTEMS(P)
GR/F34374/01 HOL VERIFICATION OF ELLA DESIGNS(P)
GR/E53262/01 HIGH LEVEL THEOREM-PROVING STRATEGIES WITH APPLICATIONS TO HARDWARE AND SOFTWARE VERIFICATION(P)
GR/E42235/01 PROGRAMMING LANGUAGE APPLICATIONS OF TYPE THEORY AND TEMPORAL LOGIC(P)
Key: (P)=Principal Investigator, (C)=Co-Investigator, (R)=Researcher Co-Investigator