Introduction to HOL: A theorem proving environment for higher order logic MJC Gordon, TF Melham Cambridge University Press, 1993 | 2732 | 1993 |
Hardware verification using higher-order logic A Camilleri, M Gordon, T Melham University of Cambridge, Computer Laboratory, 1986 | 227 | 1986 |
Automating recursive type definitions in higher order logic TF Melham Current trends in hardware verification and automated theorem proving, 341-386, 1989 | 214 | 1989 |
Higher order logic and hardware verification TF Melham Cambridge University Press, 2009 | 184 | 2009 |
Abstraction mechanisms for hardware verification TF Melham VLSI Specification, Verification and Synthesis, 267-291, 1988 | 166 | 1988 |
An industrially effective environment for formal hardware verification CJH Seger, RB Jones, JW O'Leary, T Melham, MD Aagaard, C Barrett, ... Computer-Aided Design of Integrated Circuits and Systems, IEEE Transactions …, 2005 | 130 | 2005 |
Five axioms of alpha-conversion AD Gordon, T Melham Theorem Proving in Higher Order Logics: 9th International Conference, TPHOLs …, 1996 | 127 | 1996 |
A mechanized theory of the π-calculus in HOL TF Melham University of Cambridge, Computer Laboratory, 1992 | 120 | 1992 |
A package for inductive relation definitions in HOL T Melham IEEE, 1992 | 116 | 1992 |
The PROSPER toolkit LA Dennis, G Collins, M Norrish, R Boulton, K Slind, G Robinson, ... Tools and Algorithms for the Construction and Analysis of Systems: 6th …, 2000 | 111 | 2000 |
Reasoning with inductively defined relations in the HOL theorem prover J Camilleri, T Melham Computer Laboratory ‚University of Cambridge, 1992 | 99 | 1992 |
A reflective functional language for hardware design and theorem proving J Grundy, T Melham, J O'leary Journal of Functional Programming 16 (2), 157-196, 2006 | 91 | 2006 |
Automatic heap layout manipulation for exploitation S Heelan, T Melham, D Kroening 27th USENIX Security Symposium (USENIX Security 18), 763-779, 2018 | 73 | 2018 |
Practical formal verification in microprocessor design RB Jones, JW O'Leary, CJH Seger, MD Aagaard, TF Melham IEEE design & test of computers 18 (4), 16-25, 2001 | 65 | 2001 |
Hardware verification using software analyzers R Mukherjee, D Kroening, T Melham 2015 IEEE Computer Society Annual Symposium on VLSI, 7-12, 2015 | 64 | 2015 |
Gollum: Modular and greybox exploit generation for heap overflows in interpreters S Heelan, T Melham, D Kroening Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications …, 2019 | 53 | 2019 |
Dynamic specialisation of XC6200 FPGAs by partial evaluation N McKay, T Melham, KW Susanto Proceedings. IEEE Symposium on FPGAs for Custom Computing Machines (Cat. No …, 1998 | 53 | 1998 |
Deepsynth: Automata synthesis for automatic task segmentation in deep reinforcement learning M Hasanbeig, NY Jeppu, A Abate, T Melham, D Kroening Proceedings of the AAAI Conference on Artificial Intelligence 35 (9), 7647-7656, 2021 | 52 | 2021 |
A methodology for large-scale hardware verification MD Aagaard, RB Jones, TF Melham, JW O’Leary, CJH Seger Formal Methods in Computer-Aided Design: Third International Conference …, 2000 | 52 | 2000 |
Formal co-validation of low-level hardware/software interfaces A Horn, M Tautschnig, C Val, L Liang, T Melham, J Grundy, D Kroening 2013 Formal Methods in Computer-Aided Design, 121-128, 2013 | 48 | 2013 |