| EP/K008528/1 | REMS: Rigorous Engineering for Mainstream Systems | (C) |
| 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) |