Tom Melham : Publications
|
[1] |
A Symbolic Execution Framework for Algorithm−Level Modelling Ziyad Hanna and Tom Melham In Priyank Kalla and Prabhat Mishra, editors, High Level Design Validation and Test Workshop‚ 2009. HLDVT 2009.. Pages 94–99. IEEE. 2009. |
|
[2] |
Assume−Guarantee Validation for STE Properties within an SVA Environment Zurab Khasidashvili‚ Gavriel Gavrielov and Tom Melham In Armin Biere and Carl Pixley, editors, Proceedings of 9th International Conference: 2009 Formal Methods in Computer−Aided Design: FMCAD 2009. Pages 108–115. IEEE. 2009. |
|
[3] |
Design and Verification of On−Chip Communication Protocols Peter Böhm and Tom Melham No. RR−08−05. Oxford University Computing Laboratory. April, 2008. |
|
[4] |
Design and Verification of On−Chip Communication Protocols Peter Böhm and Tom Melham In Gordon J. Pace and Satnam Singh, editors, Seventh International Workshop on Designing Correct Circuits: Budapest‚ 29–30 March 2008: Participants' Proceedings. Pages 15–29. ETAPS 2008. March, 2008. A Satellite Event of the ETAPS 2008 group of conferences |
|
[5] |
A Refinement Approach to Design and Verification of On−Chip Communication Protocols Peter Böhm and Tom Melham In Alessandro Cimatti and Robert B. Jones, editors, 2008 Formal Methods in Computer Aided Design: Portland‚ Oregon‚ USA: 17–20 November 2008. Pages 136–143. IEEE. 2008. |
|
[6] |
Early Validation of Computer Microarchitecture with Algorithm Level Models Ziyad Hanna and Tom Melham In Andreas Prinz, editor, Proceedings of ASM'07: The 14th International Abstract State Machines Workshop. 2007. Published electronically |
|
[7] |
Automatic Abstraction in Symbolic Trajectory Evaluation Sara Adams‚ Magnus Björk‚ Tom Melham and Carl−Johan Seger In Jason Baumgartner and Mary Sheeran, editors, Formal Methods in Computer Aided Design: FMCAD 2007: November 11–14 2007‚ Austin‚ Texas‚ USA. Pages 127–135. IEEE Computer Society. 2007. |
|
[8] |
A Reflective Functional Language for Hardware Design and Theorem Proving Jim Grundy‚ Tom Melham and John O'Leary In Journal of Functional Programming. Vol. 16. No. 2. Pages 157–196. March, 2006. |
|
[9] |
A Functional HDL in ReFLect Tom Melham and John O'Leary In Mary Sheeran and Tom Melham, editors, Sixth International Workshop on Designing Correct Circuits: Vienna‚ 25–26 March 2006: Participants' Proceedings. ETAPS 2006. March, 2006. A Satellite Event of the ETAPS 2006 group of conferences |
|
[10] |
Sixth International Workshop on Designing Correct Circuits: Vienna‚ 25–26 March 2006: Participants' Proceedings Mary Sheeran and Tom Melham, editors Mary Sheeran and Tom Melham, editors A Satellite Event of the ETAPS 2006 group of conferences |
|
[11] |
Tool Building Requirements for an API to First−Order Solvers Jim Grundy‚ Tom Melham‚ Sava Krstić and Sean McLaughlin In Electronic Notes in Theoretical Computer Science. Vol. 144. No. 2. Pages 15–26. January, 2006. |
|
[12] |
An Industrially Effective Environment for Formal Hardware Verification Carl−Johan H. Seger‚ Robert B. Jones‚ John W. O'Leary‚ Tom Melham‚ Mark D. Aagaard‚ Clark Barrett and Don Syme In IEEE Transactions on Computer−Aided Design of Integrated Circuits and Systems. Vol. 24. No. 9. Pages 1381–1405. September, 2005. |
|
[13] |
Theorem Proving in Higher Order Logics: 18th International Conference‚ TPHOLs 2005: Oxford‚ UK‚ August 22–25‚ 2005: Proceedings Joe Hurd and Tom Melham, editors Joe Hurd and Tom Melham, editors |
|
[14] |
Fifth International Workshop on Designing Correct Circuits: Barcelona‚ 27–28 March 2004: Participants' Proceedings Tom Melham and Mary Sheeran, editors Tom Melham and Mary Sheeran, editors A Satellite Event of the ETAPS 2004 group of conferences |
|
[15] |
Integrating Model Checking and Theorem Proving in a Reflective Functional Language Tom Melham In Eerke A. Boiten‚ John Derrick and Graeme Smith, editors, Integrated Formal Methods: 4th International Conference‚ IFM 2004: Canterbury‚ UK‚ April 4–7‚ 2004: Proceedings. Vol. 2999 of Lecture Notes in Computer Science. Pages 36–39. Springer−Verlag. 2004. |
|
[16] |
The PROSPER toolkit Louise A. Dennis‚ Graham Collins‚ Michael Norrish‚ Richard J. Boulton‚ Konrad Slind and Thomas F. Melham In International Journal on Software Tools for Technology Transfer. Vol. 4. No. 2. Pages 189–210. February, 2003. |
|
[17] |
A Reflective Functional Language for Hardware Design and Theorem Proving Jim Grundy‚ Tom Melham and John O'Leary No. PRG−RR−03−16. Programming Research Group‚ Oxford University Computing Laboratory. October, 2003. |
|
[18] |
Abstract: Experience with Practical Formal Verification at an Industrial Scale Tom Melham In Clare Dixon, editor, Proceedings of the Tenth Workshop on Automated Reasoning: Bridging the Gap between Theory and Practice: 15th–16th April 2003: Liverpool. Pages 1–2. Department of Computer Science‚ University of Liverpool. 2003. |
|
[19] |
An AMBA−ARM7 Formal Verification Platform Kong Woei Susanto and Tom Melham In Jin Song Dong and Jim Woodcock, editors, Formal Methods and Software Engineering: 5th International Conference on Formal Engineering Methods‚ ICFEM 2003: Singapore‚ November 5–7‚ 2003: Proceedings. Vol. 2885 of Lecture Notes in Computer Science. Pages 48–67. Springer−Verlag. 2003. |
|
[20] |
Designing Correct Circuits (DCC'02) Mary Sheeran and Tom Melham, editors Mary Sheeran and Tom Melham, editors Proceedings of the Workshop on Designing Correct Circuits held during 6–7 April 2002 in Grenoble‚ France |
|
[21] |
PROSPER: An Investigation into Software Architecture for Embedded Proof Engines Thomas F. Melham In Alessandro Armando, editor, Frontiers of Combining Systems: 4th International Workshop‚ FroCoS 2002: Santa Margherita Ligure‚ Italy‚ April 8–10‚ 2002: Proceedings. Vol. 2309 of Lecture Notes in Artificial Intelligence. Pages 193–206. Springer−Verlag. 2002. |
|
[22] |
Abstraction by Symbolic Indexing Transformations Thomas F. Melham and Robert B. Jones In Mark D. Aagaard and John W. O'Leary, editors, Formal Methods in Computer−Aided Design: 4th International Conference‚ FMCAD 2002: Portland‚ OR‚ USA‚ November 6–8‚ 2002: Proceedings. Vol. 2517 of Lecture Notes in Computer Science. Pages 1–18. Springer−Verlag. 2002. |
|
[23] |
Formally Analyzed Dynamic Synthesis of Hardware Kong Woei Susanto and Tom Melham In The Journal of Supercomputing. Vol. 19. No. 1. Pages 7–22. May, 2001. |
|
[24] |
Practical Formal Verification in Microprocessor Design Robert B. Jones‚ John W. O'Leary‚ Carl−Johan H. Seger‚ Mark D. Aagaard and Thomas F. Melham In IEEE Design & Test of Computers. Vol. 18. No. 4. Pages 16–25. , 2001. |
|
[25] |
Correct Hardware Design and Verification Methods: 11th IFIP WG10.5 Advanced Research Working Conference‚ CHARME 2001: Livingston‚ Scotland‚ UK‚ September 4–7 2001: Proceedings Tiziana Margaria and Tom Melham, editors Tiziana Margaria and Tom Melham, editors |
|
[26] |
An analysis of errors in interactive proof attempts S. Aitken and T. Melham In Interacting with Computers. Vol. 12. No. 6. Pages 565–586. June, 2000. |
|
[27] |
Xs are for Trajectory Evaluation‚ Booleans are for Theorem Proving (Extended Version) Mark D. Aagaard‚ Thomas F. Melham and John W. O'Leary No. TR−2000−52. Department of Computing Science‚ University of Glasgow. January, 2000. |
|
[28] |
The PROSPER Toolkit Louise A. Dennis‚ Graham Collins‚ Michael Norrish‚ Richard Boulton‚ Konrad Slind‚ Graham Robinson‚ Mike Gordon and Tom Melham In Susanne Graf and Michael Schwartzbach, editors, Tools and Algorithms for the Construction and Analysis of Systems: 6th International Conference‚ TACAS 2000: Held as Part of the Joint European Conferences on Theory and Practice of Software‚ ETAPS 2000: Berlin‚ Germany‚ March 25 – April 2‚ 2000: Proceedings. Vol. 1785 of Lecture Notes in Computer Science. Pages 78–92. Springer−Verlag. 2000. |
|
[29] |
A Methodology for Large−Scale Hardware Verification Mark D. Aagaard‚ Robert B. Jones‚ Thomas F. Melham‚ John W. O'Leary and Carl−Johan H. Seger In Jr. Warren A. Hunt and Steven D. Johnson, editors, Formal Methods in Computer−Aided Design: Third International Conference‚ FMCAD 2000: Austin‚ TX‚ USA‚ November 1–3‚ 2000: Proceedings. Vol. 1954 of Lecture Notes in Computer Science. Pages 263–282. Springer−Verlag. 2000. |
|
[30] |
Xs Are for Trajectory Evaluation‚ Booleans Are for Theorem Proving Mark D. Aagaard‚ Thomas F. Melham and John W. O'Leary In Laurence Pierre and Thomas Kropf, editors, Correct Hardware Design and Verification Methods: 10th IFIP WG10.5 Advanced Research Working Conference‚ CHARME'99: Bad Herrenalb‚ Germany‚ September 27–29‚ 1999: Proceedings. Vol. 1703 of Lecture Notes in Computer Science. Pages 202–218. Springer−Verlag. 1999. |
|
[31] |
Interactive Theorem Proving: An Empirical Study of User Activity J. S. Aitken‚ P. Gray‚ T. Melham and M. Thomas In Journal of Symbolic Computation. Vol. 25. No. 2. Pages 263–284. February, 1998. |
|
[32] |
Formally Analysed Dynamic Synthesis of Hardware Kong Woei Susanto and Tom Melham In Jim Grundy and Malcolm Newey, editors, Theorem Proving in Higher Order Logics: Emerging Trends: 11th International Conference‚ TPHOLs'98‚ Canberra‚ September 27 – October 1‚ 1998: Supplementary Proceedings. Pages 105–117. Australian National University. 1998. |
|
[33] |
Dynamic Specialisation of XC6200 FPGAs by Partial Evaluation Nicholas McKay‚ Tom Melham‚ Kong Woei Susanto and Satnam Singh In Kenneth L. Pocek and Jeffrey M. Arnold, editors, Proceedings: IEEE Symposium on FPGAs for Custom Computing Machines: April 15–17‚ 1998‚ Napa Valley‚ California. Pages 308–309. IEEE Computer Society. 1998. |
|
[34] |
ITP Project Anthology Stuart Aitken‚ Philip Gray‚ Tom Melham and Muffy Thomas No. TR−1997−36. Department of Computing Science‚ University of Glasgow. November, 1997. |
|
[35] |
Some Research Issues in Higher Order Logic Theorem Proving Tom F. Melham No. NS−96−7. Department of Computer Science‚ University of Aarhus. October, 1996. |
|
[36] |
Phases‚ Modes and Information Flow in Theory Development J. S. Aitken‚ P. Gray‚ T. Melham and M. Thomas In Nicholas A. Merriam, editor, User Interfaces for Theorem Provers: An International Workshop organised at the Department of Computer Science‚ University of York: 19th July 1996. Pages 1–8. University of York. 1996. |
|
[37] |
Five Axioms of Alpha−Conversion Andrew D. Gordon and Tom Melham In J. von Wright‚ J. Grundy and J. Harrison, editors, Theorem Proving in Higher Order Logics: 9th International Conference‚ TPHOLs'96: Turku‚ Finland‚ August 26–30‚ 1996: Proceedings. Vol. 1125 of Lecture Notes in Computer Science. Pages 173–190. Springer−Verlag. 1996. |
|
[38] |
A Study Of User Activity In Interactive Theorem Proving Stuart Aitken‚ Philip Gray‚ Tom Melham and Muffy Thomas In Chris Johnson, editor, Task Centred Approaches To Interface Design: Glasgow Interactive Systems Group Research Review. Pages 195–218. Department of Computing Science‚ University of Glasgow. August, 1995. GIST Technical Report G95.2 |
|
[39] |
Interactive Proof Discovery: An Empirical Study of HOL Users Stuart Aitken‚ Philip Gray‚ Tom Melham and Muffy Thomas In Philip Gray, editor, User Interface Design for Theorem Proving Systems: An International Workshop organised by the ITP Project. Department of Computing Science‚ University of Glasgow. 1995. |
|
[40] |
Supplementary Proceedings of the 7th International Workshop on Higher Order Logic Theorem Proving and its Applications Tom Melham and Juanito Camilleri, editors Tom Melham and Juanito Camilleri, editors |
|
[41] |
The HOL Logic Extended with Quantification over Type Variables Thomas F. Melham In Formal Methods in System Design. Vol. 3. No. 1–2. Pages 7–24. 1994. |
|
[42] |
A Mechanized Theory of the Π−calculus in HOL T. F. Melham In Nordic Journal of Computing. Vol. 1. No. 1. Pages 50–76. 1994. |
|
[43] |
Higher Order Logic Theorem Proving and Its Applications: 7th International Workshop: Valletta‚ Malta‚ September 19–22‚ 1994: Proceedings Thomas F. Melham and Juanito Camilleri, editors Thomas F. Melham and Juanito Camilleri, editors |
|
[44] |
Introduction to HOL: A theorem proving environment for higher order logic M. J. C. Gordon and T. F. Melham, editors Cambridge University Press. 1993. |
|
[45] |
Higher Order Logic and Hardware Verification T. Melham Vol. 31 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press. 1993. |
|
[46] |
Translating Dependent Type Theory into Higher Order Logic Bart Jacobs and Tom Melham In M. Bezem and J. F. Groote, editors, Typed Lambda Calculi and Applications: International Conference on Typed Lamda Calculi and Applications: TLCA '93: March‚ 16–18‚ 1993‚ Utrecht‚ The Netherlands: Proceedings. Vol. 664 of Lecture Notes in Computer Science. Pages 209–229. Springer−Verlag. 1993. |
|
[47] |
The HOL Logic Extended with Quantification over Type Variables Thomas F. Melham In Luc J. M. Claesen and Michael J. C. Gordon, editors, Higher Order Logic Theorem Proving and its Applications: Proceedings of the IFIP TC10/WG10.2 International Workshop on Higher Order Logic Theorem Proving and its Applications − HOL '92: Leuven‚ Belgium‚ 21–24 September 1992. Vol. 20 of IFIP Transactions A. Pages 3–17. North−Holland. 1993. |
|
[48] |
Reasoning with Inductively Defined Relations in the HOL Theorem Prover Juanito Camilleri and Tom Melham No. 265. Computer Laboratory‚ University of Cambridge. August, 1992. |
|
[49] |
The HOL pred_sets Library Computer Laboratory‚ University of Cambridge. Computer Laboratory‚ University of Cambridge. February, 1992. |
|
[50] |
The HOL finite_sets Library Computer Laboratory‚ University of Cambridge. Computer Laboratory‚ University of Cambridge. February, 1992. |
|
[51] |
A Mechanized Theory of the π−calculus in HOL T. F. Melham No. 244. Computer Laboratory‚ University of Cambridge. January, 1992. |
|
[52] |
A Package for Inductive Relation Definitions in HOL T. F. Melham In Myla Archer‚ Jeffrey J. Joyce‚ Karl N. Levitt and Phillip J. Windley, editors, Proceedings of the 1991 International Workshop on the HOL Theorem Proving System and its Applications‚ Davis‚ California‚ August 28–30‚ 1991. Pages 350–357. IEEE Computer Society Press. 1992. |
|
[53] |
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 V. Stavridou‚ T. F. Melham and R. T. Boute, editors V. Stavridou‚ T. F. Melham and R. T. Boute, editors |
|
[54] |
The HOL string Library Computer Laboratory‚ University of Cambridge. Computer Laboratory‚ University of Cambridge. June, 1991. |
|
[55] |
The HOL sets Library Computer Laboratory‚ University of Cambridge. Computer Laboratory‚ University of Cambridge. October, 1991. |
|
[56] |
A Mechanized Theory of the π−calculus in HOL T. F. Melham In G. Huet and G. Plotkin, editors, Proceedings of the Second Workshop on Logical Frameworks. Pages 219–237. University of Edinburgh. 1991. Preliminary proceedings‚ published electronically after the workshop |
|
[57] |
Abstraction Mechanisms for Hardware Verification Thomas F. Melham In Michael Yoeli, editor, Formal Verification of Hardware Design. Pages 30–49. IEEE Computer Society Press. 1990. |
|
[58] |
Formalizing Abstraction Mechanisms for Hardware Verification in Higher Order Logic Thomas Frederick Melham PhD Thesis University of Cambridge. August, 1989. |
|
[59] |
Automating Recursive Type Definitions in Higher Order Logic Thomas F. Melham In G. Birtwistle and P. A. Subrahmanyam, editors, Current Trends in Hardware Verification and Automated Theorem Proving. Pages 341–386. Springer−Verlag. 1989. |
|
[60] |
Automating Recursive Type Definitions in Higher Order Logic Thomas F. Melham No. 146. Computer Laboratory‚ University of Cambridge. September, 1988. |
|
[61] |
Using Recursive Types to Reason about Hardware in Higher Order Logic Thomas F. Melham No. 135. Computer Laboratory‚ University of Cambridge. May, 1988. |
|
[62] |
Hardware Verification by Formal Proof Graham Birtwistle‚ Brian Graham‚ Tom Melham and Rick Schediwy No. 88/328/40. Department of Computer Science‚ University of Calgary. October, 1988. |
|
[63] |
Hardware Verification by Formal Proof G. Birtwistle‚ B. Graham‚ T. Melham and R. Schediwy In V. K. Bhargava, editor, Proceedings of the Canadian Conference on Electrical and Computer Engineering‚ Vancouver‚ November 1988. Pages 379–384. Canadian Society for Electrical Engineering. 1988. |
|
[64] |
Using Recursive Types to Reason about Hardware in Higher Order Logic Thomas F. Melham In George J. Milne, editor, The Fusion of Hardware Design and Verification: Proceedings of the IFIP WG 10.2 Working Conference on The Fusion of Hardware Design and Verification: Glasgow‚ Scotland‚ 4–6 July‚ 1988. Pages 27–50. North−Holland. 1988. |
|
[65] |
Abstraction Mechanisms for Hardware Verification Thomas F. Melham In Graham Birtwistle and P. A. Subrahmanyam, editors, VLSI Specification‚ Verification and Synthesis. Vol. SECS35 of The Kluwer International Series in Engineeering and Computer Science. Pages 267–291. Kluwer Academic Publishers. 1988. |
|
[66] |
Abstraction Mechanisms for Hardware Verification Thomas F. Melham No. 106. Computer Laboratory‚ University of Cambridge. May, 1987. |
|
[67] |
Hardware Verification using Higher−Order Logic Albert Camilleri‚ Mike Gordon and Tom Melham In Dominique Borrione, editor, From HDL Descriptions to Guaranteed Correct Circuit Designs: Proceedings of the IFIP WG 10.2 Working Conference on From HDL Descriptions to Guaranteed Correct Circuit Designs‚ Grenoble‚ France‚ 9–11 September‚ 1986. Pages 43–67. North−Holland. 1987. |
|
[68] |
Hardware Verification using Higher−Order Logic Albert Camilleri‚ Mike Gordon and Tom Melham No. 91. Computer Laboratory‚ University of Cambridge. June, 1986. |
|
[69] |
Specification and VLSI Design Graham Birtwistle‚ Jeff Joyce‚ Breen Liblong‚ Tom Melham and Rick Schediwy In George J. Milne and P. A. Subrahmanyam, editors, Formal Aspects of VLSI Design: Proceedings of the 1985 Edinburgh Workshop on VLSI: Edinburgh‚ Scotland‚ U.K.. Pages 83–97. North−Holland. 1986. |
|
[70] |
Towards a VLSI Design Tool System Breen Liblong‚ Tom Melham‚ Graham Birtwistle and John Kendall In INFOR: Information Systems and Operational Research. Vol. 23. No. 4. Pages 389–402. November, 1985. |
|
[71] |
Specification and VLSI Design Graham Birtwistle‚ Jeff Joyce‚ Breen Liblong‚ Tom Melham and Rick Schediwy No. 85/220/33. Department of Computer Science‚ University of Calgary. November, 1985. |
|
[72] |
EDICT: An Environment for Design Using Integrated Circuit Tools Graham Birtwistle‚ David Hill‚ John Kendall‚ Bill Coates‚ Richard Esau‚ Wallace Kroeker‚ Breen Liblong‚ Erwin Liu‚ Tom Melham and Rick Schediwy No. 84/155/13. Department of Computer Science‚ University of Calgary. June, 1984. |
|
[73] |
Towards a VLSI Design Tool System Breen Liblong‚ Tom Melham‚ Graham Birtwistle and John Kendall No. 84/175/33. Department of Computer Science‚ University of Calgary. November, 1984. |
|
[74] |
Exploiting Hierarchies in EDICT B. Liblong‚ T. Melham and G. Birtwistle In Proceedings of the 1984 Canadian Conference on VLSI. 1984. |
|
[75] |
Towards a VLSI Design Tool System Breen Liblong‚ Tom Melham‚ Graham Birtwistle and John Kendall In Leo Gotlieb, editor, Canadian Information Processing Society: SESSION 84: Proceedings. Pages 37–42. Canadian Information Processing Society. 1984. |