Thomas F. Melham

30 papers A* 1A 1B 4C 1Misc 1Journal 9Unranked 8

Year	Rank	Type	Title / Venue / Authors
2020	A*	`conf`	Learning Concise Models from Long Execution Traces. DAC Natasha Yogananda Jeppu, Thomas F. Melham, Daniel Kroening, John O'Leary
2009	—	`conf`	A symbolic execution framework for algorithm-level modelling. HLDVT Ziyad Hanna, Thomas F. Melham
2007	B	`conf`	Automatic Abstraction in Symbolic Trajectory Evaluation. FMCAD Sara Adams, Magnus Björk, Thomas F. Melham, Carl-Johan H. Seger
2006	J	`jnl`	A reflective functional language for hardware design and theorem proving. J. Funct. Program. Jim Grundy, Thomas F. Melham, John W. O'Leary
2005	J	`jnl`	An industrially effective environment for formal hardware verification. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. Carl-Johan H. Seger, Robert B. Jones, John W. O'Leary, Thomas F. Melham, Mark D. Aagaard, Clark W. Barrett, Don Syme
2005	—	`ed.`	Theorem Proving in Higher Order Logics, 18th International Conference, TPHOLs 2005, Oxford, UK, August 22-25, 2005, Proceedings TPHOLs Joe Hurd, Thomas F. Melham
2005	—	`conf`	Tool Building Requirements for an API to First-Order Solvers. PDPAR@CAV Jim Grundy, Thomas F. Melham, Sava Krstic, Sean McLaughlin
2004	B	`conf`	Integrating Model Checking and Theorem Proving in a Reflective Functional Language. IFM Thomas F. Melham
2003	C	`conf`	An AMBA-ARM7 Formal Verification Platform. ICFEM Kong Woei Susanto, Thomas F. Melham
2003	J	`jnl`	The PROSPER toolkit. Int. J. Softw. Tools Technol. Transf. Louise A. Dennis, Graham Collins, Michael Norrish, Richard J. Boulton, Konrad Slind, Thomas F. Melham
2002	B	`conf`	Abstraction by Symbolic Indexing Transformations. FMCAD Thomas F. Melham, Robert B. Jones
2002	—	`conf`	PROSPER - An Investigation into Software Architecture for Embedded Proof Engines. FroCoS Thomas F. Melham
2001	—	`ed.`	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 CHARME Tiziana Margaria, Thomas F. Melham
2001	J	`jnl`	Formally Analyzed Dynamic Synthesis of Hardware. J. Supercomput. Kong Woei Susanto, Thomas F. Melham
2001	J	`jnl`	Practical Formal Verification in Microprocessor Design. IEEE Des. Test Comput. Robert B. Jones, John W. O'Leary, Carl-Johan H. Seger, Mark D. Aagaard, Thomas F. Melham
2000	B	`conf`	A Methodology for Large-Scale Hardware Verification. FMCAD Mark D. Aagaard, Robert B. Jones, Thomas F. Melham, John W. O'Leary, Carl-Johan H. Seger
2000	J	`jnl`	An analysis of errors in interactive proof attempts. Interact. Comput. J. Stuart Aitken, Thomas F. Melham
2000	A	`conf`	The PROSPER Toolkit. TACAS Louise A. Dennis, Graham Collins, Michael Norrish, Richard J. Boulton, Konrad Slind, Graham Robinson, Michael J. C. Gordon, Thomas F. Melham
1999	—	`conf`	Xs are for Trajectory Evaluation, Booleans are for Theorem Proving. CHARME Mark D. Aagaard, Thomas F. Melham, John W. O'Leary
1998	Misc	`conf`	Dynamic Specialization of XC6200 FPGAs by Partial Evaluation. FCCM Nicholas McKay, Thomas F. Melham, Kong Woei Susanto, Satnam Singh
1998	J	`jnl`	Interactive Theorem Proving: An Empirical Study of User Activity. J. Symb. Comput. J. Stuart Aitken, Philip D. Gray, Thomas F. Melham, Muffy Thomas
1996	—	`conf`	Five Axioms of Alpha-Conversion. TPHOLs Andrew D. Gordon, Thomas F. Melham
1994	J	`jnl`	A Mechanized Theory of the Pi-Calculus in HOL. Nord. J. Comput. Thomas F. Melham
1994	—	`ed.`	Higher Order Logic Theorem Proving and Its Applications, 7th International Workshop, Valletta, Malta, September 19-22, 1994, Proceedings TPHOLs Thomas F. Melham, Juanito Camilleri
1993	—	`book`	Higher Order Logic and Hardware Verification. Thomas F. Melham
1993	J	`jnl`	The HOL Logic Extended with Quantification over Type Variables. Formal Methods Syst. Des. Thomas F. Melham
1993	—	`conf`	Translating Dependent Type Theory into Higher Order Logic. TLCA Bart Jacobs, Thomas F. Melham
1992	—	`conf`	The HOL Logic Extended with Quantification over Type Variables. TPHOLs Thomas F. Melham
1992	—	`ed.`	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 TPCD Victoria Stavridou, Thomas F. Melham, Raymond T. Boute
1991	—	`conf`	A Package for Inductive Relation Definitions in HOL. TPHOLs Thomas F. Melham