Search the dblp DataBase
Thomas F. Melham :
[Publications ]
[Author Rank by year ]
[Co-authors ]
[Prefers ]
[Cites ]
[Cited by ]
Publications of Author
Mark Aagaard , Thomas F. Melham , John W. O'Leary Xs are for Trajectory Evaluation, Booleans are for Theorem Proving. [Citation Graph (0, 0)][DBLP ] CHARME, 1999, pp:202-218 [Conf ] Nicholas McKay , Thomas F. Melham , Kong Woei Susanto , Satnam Singh Dynamic Specialization of XC6200 FPGAs by Partial Evaluation. [Citation Graph (0, 0)][DBLP ] FCCM, 1998, pp:308-309 [Conf ] Mark Aagaard , Robert B. Jones , Thomas F. Melham , John W. O'Leary , Carl-Johan H. Seger A Methodology for Large-Scale Hardware Verification. [Citation Graph (0, 0)][DBLP ] FMCAD, 2000, pp:263-282 [Conf ] Thomas F. Melham , Robert B. Jones Abstraction by Symbolic Indexing Transformations. [Citation Graph (0, 0)][DBLP ] FMCAD, 2002, pp:1-18 [Conf ] Thomas F. Melham PROSPER - An Investigation into Software Architecture for Embedded Proof Engines. [Citation Graph (0, 0)][DBLP ] FroCos, 2002, pp:193-206 [Conf ] Kong Woei Susanto , Thomas F. Melham An AMBA-ARM7 Formal Verification Platform. [Citation Graph (0, 0)][DBLP ] ICFEM, 2003, pp:48-67 [Conf ] Thomas F. Melham Integrating Model Checking and Theorem Proving in a Reflective Functional Language. [Citation Graph (0, 0)][DBLP ] IFM, 2004, pp:36-39 [Conf ] Louise A. Dennis , Graham Collins , Michael Norrish , Richard J. Boulton , Konrad Slind , Graham Robinson , Michael J. C. Gordon , Thomas F. Melham The PROSPER Toolkit. [Citation Graph (0, 0)][DBLP ] TACAS, 2000, pp:78-92 [Conf ] Bart Jacobs , Thomas F. Melham Translating Dependent Type Theory into Higher Order Logic. [Citation Graph (0, 0)][DBLP ] TLCA, 1993, pp:209-229 [Conf ] Andrew D. Gordon , Thomas F. Melham Five Axioms of Alpha-Conversion. [Citation Graph (0, 0)][DBLP ] TPHOLs, 1996, pp:173-190 [Conf ] Thomas F. Melham A Package for Inductive Relation Definitions in HOL. [Citation Graph (0, 0)][DBLP ] TPHOLs, 1991, pp:350-357 [Conf ] Thomas F. Melham The HOL Logic Extended with Quantification over Type Variables. [Citation Graph (0, 0)][DBLP ] TPHOLs, 1992, pp:3-17 [Conf ] Robert B. Jones , John W. O'Leary , Carl-Johan H. Seger , Mark Aagaard , Thomas F. Melham Practical Formal Verification in Microprocessor Design. [Citation Graph (0, 0)][DBLP ] IEEE Design & Test of Computers, 2001, v:18, n:4, pp:16-25 [Journal ] Jim Grundy , Thomas F. Melham , Sava Krstic , Sean McLaughlin Tool Building Requirements for an API to First-Order Solvers. [Citation Graph (0, 0)][DBLP ] Electr. Notes Theor. Comput. Sci., 2006, v:144, n:2, pp:15-26 [Journal ] Thomas F. Melham The HOL Logic Extended with Quantification over Type Variables. [Citation Graph (0, 0)][DBLP ] Formal Methods in System Design, 1993, v:3, n:1/2, pp:7-24 [Journal ] J. Stuart Aitken , Thomas F. Melham An analysis of errors in interactive proof attempts. [Citation Graph (0, 0)][DBLP ] Interacting with Computers, 2000, v:12, n:6, pp:565-586 [Journal ] Jim Grundy , Thomas F. Melham , John W. O'Leary A reflective functional language for hardware design and theorem proving. [Citation Graph (0, 0)][DBLP ] J. Funct. Program., 2006, v:16, n:2, pp:157-196 [Journal ] J. Stuart Aitken , Philip D. Gray , Thomas F. Melham , Muffy Thomas Interactive Theorem Proving: An Empirical Study of User Activity. [Citation Graph (0, 0)][DBLP ] J. Symb. Comput., 1998, v:25, n:2, pp:263-284 [Journal ] Thomas F. Melham A Mechanized Theory of the Pi-Calculus in HOL. [Citation Graph (0, 0)][DBLP ] Nord. J. Comput., 1994, v:1, n:1, pp:50-76 [Journal ] Louise A. Dennis , Graham Collins , Michael Norrish , Richard J. Boulton , Konrad Slind , Thomas F. Melham The PROSPER toolkit. [Citation Graph (0, 0)][DBLP ] STTT, 2003, v:4, n:2, pp:189-210 [Journal ] 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. [Citation Graph (0, 0)][DBLP ] IEEE Trans. on CAD of Integrated Circuits and Systems, 2005, v:24, n:9, pp:1381-1405 [Journal ] Kong Woei Susanto , Thomas F. Melham Formally Analyzed Dynamic Synthesis of Hardware. [Citation Graph (0, 0)][DBLP ] The Journal of Supercomputing, 2001, v:19, n:1, pp:7-22 [Journal ] Automatic Abstraction in Symbolic Trajectory Evaluation. [Citation Graph (, )][DBLP ] Search in 0.042secs, Finished in 0.044secs