 | 2007 |
| 27 |  | Sara Adams,
Magnus Björk,
Thomas F. Melham,
Carl-Johan H. Seger:
Automatic Abstraction in Symbolic Trajectory Evaluation.
FMCAD 2007: 127-135 |
| 2006 |
| 26 |  | Jim Grundy,
Thomas F. Melham,
Sava Krstic,
Sean McLaughlin:
Tool Building Requirements for an API to First-Order Solvers.
Electr. Notes Theor. Comput. Sci. 144(2): 15-26 (2006) |
| 25 |  | Jim Grundy,
Thomas F. Melham,
John W. O'Leary:
A reflective functional language for hardware design and theorem proving.
J. Funct. Program. 16(2): 157-196 (2006) |
| 2005 |
| 24 |  | Joe Hurd,
Thomas F. Melham:
Theorem Proving in Higher Order Logics, 18th International Conference, TPHOLs 2005, Oxford, UK, August 22-25, 2005, Proceedings
Springer 2005 |
| 23 |  | Carl-Johan H. Seger,
Robert B. Jones,
John W. O'Leary,
Thomas F. Melham,
Mark Aagaard,
Clark Barrett,
Don Syme:
An industrially effective environment for formal hardware verification.
IEEE Trans. on CAD of Integrated Circuits and Systems 24(9): 1381-1405 (2005) |
| 2004 |
| 22 |  | Thomas F. Melham:
Integrating Model Checking and Theorem Proving in a Reflective Functional Language.
IFM 2004: 36-39 |
| 2003 |
| 21 |  | Kong Woei Susanto,
Thomas F. Melham:
An AMBA-ARM7 Formal Verification Platform.
ICFEM 2003: 48-67 |
| 20 |  | Louise A. Dennis,
Graham Collins,
Michael Norrish,
Richard J. Boulton,
Konrad Slind,
Thomas F. Melham:
The PROSPER toolkit.
STTT 4(2): 189-210 (2003) |
| 2002 |
| 19 |  | Thomas F. Melham,
Robert B. Jones:
Abstraction by Symbolic Indexing Transformations.
FMCAD 2002: 1-18 |
| 18 |  | Thomas F. Melham:
PROSPER - An Investigation into Software Architecture for Embedded Proof Engines.
FroCos 2002: 193-206 |
| 2001 |
| 17 |  | Tiziana Margaria,
Thomas F. Melham:
Correct Hardware Design and Verification Methods, 11th IFIP WG 10.5 Advanced Research Working Conference, CHARME 2001, Livingston, Scotland, UK, September 4-7, 2001, Proceedings
Springer 2001 |
| 16 |  | Robert B. Jones,
John W. O'Leary,
Carl-Johan H. Seger,
Mark Aagaard,
Thomas F. Melham:
Practical Formal Verification in Microprocessor Design.
IEEE Design & Test of Computers 18(4): 16-25 (2001) |
| 15 |  | Kong Woei Susanto,
Thomas F. Melham:
Formally Analyzed Dynamic Synthesis of Hardware.
The Journal of Supercomputing 19(1): 7-22 (2001) |
| 2000 |
| 14 |  | Mark Aagaard,
Robert B. Jones,
Thomas F. Melham,
John W. O'Leary,
Carl-Johan H. Seger:
A Methodology for Large-Scale Hardware Verification.
FMCAD 2000: 263-282 |
| 13 |  | Louise A. Dennis,
Graham Collins,
Michael Norrish,
Richard J. Boulton,
Konrad Slind,
Graham Robinson,
Michael J. C. Gordon,
Thomas F. Melham:
The PROSPER Toolkit.
TACAS 2000: 78-92 |
| 12 |  | J. Stuart Aitken,
Thomas F. Melham:
An analysis of errors in interactive proof attempts.
Interacting with Computers 12(6): 565-586 (2000) |
| 1999 |
| 11 |  | Mark Aagaard,
Thomas F. Melham,
John W. O'Leary:
Xs are for Trajectory Evaluation, Booleans are for Theorem Proving.
CHARME 1999: 202-218 |
| 1998 |
| 10 |  | Nicholas McKay,
Thomas F. Melham,
Kong Woei Susanto,
Satnam Singh:
Dynamic Specialization of XC6200 FPGAs by Partial Evaluation.
FCCM 1998: 308-309 |
| 9 |  | J. Stuart Aitken,
Philip D. Gray,
Thomas F. Melham,
Muffy Thomas:
Interactive Theorem Proving: An Empirical Study of User Activity.
J. Symb. Comput. 25(2): 263-284 (1998) |
| 1996 |
| 8 |  | Andrew D. Gordon,
Thomas F. Melham:
Five Axioms of Alpha-Conversion.
TPHOLs 1996: 173-190 |
| 1994 |
| 7 |  | Thomas F. Melham,
Juanito Camilleri:
Higher Order Logic Theorem Proving and Its Applications, 7th International Workshop, Valletta, Malta, September 19-22, 1994, Proceedings
Springer 1994 |
| 6 |  | Thomas F. Melham:
A Mechanized Theory of the Pi-Calculus in HOL.
Nord. J. Comput. 1(1): 50-76 (1994) |
| 1993 |
| 5 |  | Bart Jacobs,
Thomas F. Melham:
Translating Dependent Type Theory into Higher Order Logic.
TLCA 1993: 209-229 |
| 4 |  | Thomas F. Melham:
The HOL Logic Extended with Quantification over Type Variables.
Formal Methods in System Design 3(1/2): 7-24 (1993) |
| 1992 |
| 3 |  | Victoria Stavridou,
Thomas F. Melham,
Raymond T. Boute:
Theorem Provers in Circuit Design, Proceedings of the IFIP TC10/WG 10.2 International Conference on Theorem Provers in Circuit Design: Theory, Practice and Experience, Nijmegen, The Netherlands, 22-24 June 1992, Proceedings
North-Holland 1992 |
| 2 |  | Thomas F. Melham:
The HOL Logic Extended with Quantification over Type Variables.
TPHOLs 1992: 3-17 |
| 1991 |
| 1 |  | Thomas F. Melham:
A Package for Inductive Relation Definitions in HOL.
TPHOLs 1991: 350-357 |