Tom Melham - Publications

Here is a list of my scientific publications. Many items have links to electronic copies of the articles; please contact me for help with any item you're having difficulty getting a copy of. There is also a complete BiBTeX file of all my publications. See also my entries in the DBLP Bibliography Server or Google Scholar.

Books

[1] T. Melham. Higher Order Logic and Hardware Verification, volume 31 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1993. [ bib | DOI | .html ]

Refereed Articles

[2] Rajdeep Mukherjee, Peter Schrammel, Leopold Haller, Daniel Kroening, and Tom Melham. Lifting CDCL to template-based abstract domains for program verification. In Deepak D'Souza and K. Narayan Kumar, editors, Automated Technology for Verification and Analysis: 15th International Symposium, ATVA 2017, Pune, India, October 3–6, 2017, Proceedings, volume 10482 of Lecture Notes in Computer Science, pages 307-326. Springer, Cham, 2017. [ bib | DOI | .pdf ]
[3] Lihao Liang, Tom Melham, Daniel Kroening, Peter Schrammel, and Michael Tautschnig. Effective verification for low-level software with competing interrupts. ACM Transactions on Embedded Computing Systems, 2017. [ bib ]
[4] Rajdeep Mukherjee, Peter Schrammel, Daniel Kroening, and Tom Melham. Unbounded safety verification for hardware using software analyzers. In Luca Fanucci and Jürgen Teich, editors, 2016 Design, Automation & Test in Europe Conference & Exhibition, DATE 2016, Dresden, Germany, March 14-18, 2016, pages 1152-1155. European Design and Automation Association, 2016. [ bib | DOI | .pdf ]
[5] Rajdeep Mukherjee, Saurabh Joshi, Andreas Griesmayer, Daniel Kroening, and Tom Melham. Equivalence checking of a floating-point unit against a high-level C model. In John S. Fitzgerald, Constance L. Heitmeyer, Stefania Gnesi, and Anna Philippou, editors, FM 2016: Formal Methods - 21st International Symposium, Limassol, Cyprus, November 9-11, 2016, Proceedings, volume 9995 of Lecture Notes in Computer Science, pages 551-558. Springer-Verlag, 2016. [ bib | DOI ]
[6] Peter Schrammel, Tom Melham, and Daniel Kroening. Generating test case chains for reactive systems. International Journal on Software Tools for Technology Transfer, 18(3):319-334, June 2016. [ bib | DOI | .pdf ]
[7] Rajdeep Mukherjee, Daniel Kroening, and Tom Melham. Hardware verification using software analyzers. In 2015 IEEE Computer Society Annual Symposium on VLSI, ISVLSI 2015, Montpellier, France, July 8-10, 2015, pages 7-12. IEEE Computer Society, 2015. [ bib | DOI ]
[8] Rajdeep Mukherjee, Daniel Kroening, Tom Melham, and Mandayam K. Srivas. Equivalence checking using trace partitioning. In 2015 IEEE Computer Society Annual Symposium on VLSI, ISVLSI 2015, Montpellier, France, July 8-10, 2015, pages 13-18. IEEE Computer Society, 2015. [ bib | DOI ]
[9] Daniel Kroening, Lihao Liang, Tom Melham, Peter Schrammel, and Michael Tautschnig. Effective verification of low-level software with nested interrupts. In Wolfgang Nebel and David Atienza, editors, Proceedings of the 2015 Design, Automation & Test in Europe Conference & Exhibition, DATE 2015, Grenoble, France, March 9-13, 2015, pages 229-234. EDA Consortium, 2015. [ bib | .pdf ]
[10] Peter Schrammel, Tom Melham, and Daniel Kroening. Chaining test cases for reactive system testing. In Hüsnü Yenigün, Cemal Yilmaz, and Andreas Ulrich, editors, Testing Software and Systems - 25th IFIP WG 6.1 International Conference, ICTSS 2013, Istanbul, Turkey, November 13-15, 2013, Proceedings, volume 8254 of Lecture Notes in Computer Science, pages 133-148. Springer Verlag, November 2013. [ bib | DOI | .pdf ]
[11] Alex Horn, Michael Tautschnig, Celina Val, Liaho Liang, Tom Melham, Jim Grundy, and Daniel Kroening. Formal co-validation of low-level hardware/software interfaces. In Barbara Jobstmann and Sandip Ray, editors, FMCAD 2013: Formal Methods in Computer-Aided Design: Portland, Oregon, USA, 20-23 October 2013, pages 121-128. IEEE, 2013. [ bib ]
[12] John O'Leary, Roope Kaivola, and Tom Melham. Relational STE and theorem proving for formal verification of industrial circuit designs. In Barbara Jobstmann and Sandip Ray, editors, FMCAD 2013: Formal Methods in Computer-Aided Design: Portland, Oregon, USA, 20-23 October 2013, pages 97-104. IEEE, 2013. [ bib ]
[13] Tom Melham. Modelling, abstraction, and computation in systems biology: A view from computer science. Progress in Biophysics and Molecular Biology, 111(2-3):129-136, April 2013. Focussed Issue: Conceptual Foundations of Systems Biology. [ bib | DOI ]
[14] Zurab Khasidashvili, Gavriel Gavrielov, and Tom Melham. Assume-guarantee validation for STE properties within an SVA environment. 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. [ bib | DOI | .pdf ]
[15] Peter Böhm and Tom Melham. A refinement approach to design and verification of on-chip communication protocols. 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. [ bib | DOI | .pdf ]
[16] Sara Adams, Magnus Björk, Tom Melham, and Carl-Johan Seger. Automatic abstraction in symbolic trajectory evaluation. 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. [ bib | DOI | .pdf ]
[17] Ziyad Hanna and Tom Melham. Early validation of computer microarchitecture with algorithm level models. In Andreas Prinz, editor, Proceedings of ASM'07: The 14th International Abstract State Machines Workshop, 2007. Published electronically. [ bib | .pdf ]
[18] Jim Grundy, Tom Melham, and John O'Leary. A reflective functional language for hardware design and theorem proving. Journal of Functional Programming, 16(2):157-196, March 2006. [ bib | DOI | .pdf ]
[19] Jim Grundy, Tom Melham, Sava Krstić, and Sean McLaughlin. Tool building requirements for an api to first-order solvers. Electronic Notes in Theoretical Computer Science, 144(2):15-26, January 2006. [ bib | DOI | .pdf ]
[20] Carl-Johan H. Seger, Robert B. Jones, John W. O'Leary, Tom Melham, Mark D. Aagaard, Clark Barrett, and Don Syme. An industrially effective environment for formal hardware verification. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 24(9):1381-1405, September 2005. [ bib | DOI | .pdf ]
[21] Kong Woei Susanto and Tom Melham. An AMBA-ARM7 formal verification platform. 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, volume 2885 of Lecture Notes in Computer Science, pages 48-67. Springer-Verlag, 2003. [ bib | .pdf ]
[22] Louise A. Dennis, Graham Collins, Michael Norrish, Richard J. Boulton, Konrad Slind, and Thomas F. Melham. The PROSPER toolkit. International Journal on Software Tools for Technology Transfer, 4(2):189-210, February 2003. [ bib | DOI | http ]
[23] Thomas F. Melham and Robert B. Jones. Abstraction by symbolic indexing transformations. 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, volume 2517 of Lecture Notes in Computer Science, pages 1-18. Springer-Verlag, 2002. [ bib | .pdf ]
[24] Robert B. Jones, John W. O'Leary, Carl-Johan H. Seger, Mark D. Aagaard, and Thomas F. Melham. Practical formal verification in microprocessor design. IEEE Design & Test of Computers, 18(4):16-25, July/August 2001. [ bib | DOI | .pdf ]
[25] Kong Woei Susanto and Tom Melham. Formally analyzed dynamic synthesis of hardware. The Journal of Supercomputing, 19(1):7-22, May 2001. [ bib | DOI | .ps ]
[26] Mark D. Aagaard, Robert B. Jones, Thomas F. Melham, John W. O'Leary, and Carl-Johan H. Seger. A methodology for large-scale hardware verification. In Warren A. Hunt, Jr. and Steven D. Johnson, editors, Formal Methods in Computer-Aided Design: Third International Conference, FMCAD 2000: Austin, TX, USA, November 1-3, 2000: Proceedings, volume 1954 of Lecture Notes in Computer Science, pages 263-282. Springer-Verlag, 2000. [ bib | .pdf ]
[27] S. Aitken and T. Melham. An analysis of errors in interactive proof attempts. Interacting with Computers, 12(6):565-586, June 2000. [ bib ]
[28] Louise A. Dennis, Graham Collins, Michael Norrish, Richard Boulton, Konrad Slind, Graham Robinson, Mike Gordon, and Tom Melham. The PROSPER toolkit. 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, volume 1785 of Lecture Notes in Computer Science, pages 78-92. Springer-Verlag, 2000. [ bib | .pdf ]
[29] Mark D. Aagaard, Thomas F. Melham, and John W. O'Leary. Xs are for trajectory evaluation, Booleans are for theorem proving. 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, volume 1703 of Lecture Notes in Computer Science, pages 202-218. Springer-Verlag, 1999. [ bib | .pdf ]
[30] Nicholas McKay, Tom Melham, Kong Woei Susanto, and Satnam Singh. Dynamic specialisation of XC6200 FPGAs by partial evaluation. 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. [ bib | .pdf ]
[31] J. S. Aitken, P. Gray, T. Melham, and M. Thomas. Interactive theorem proving: An empirical study of user activity. Journal of Symbolic Computation, 25(2):263-284, February 1998. [ bib ]
[32] Andrew D. Gordon and Tom Melham. Five axioms of alpha-conversion. 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, volume 1125 of Lecture Notes in Computer Science, pages 173-190. Springer-Verlag, 1996. [ bib | .pdf ]
[33] J. S. Aitken, P. Gray, T. Melham, and M. Thomas. Phases, modes and information flow in theory development. 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. [ bib ]
[34] T. F. Melham. A mechanized theory of the Π-calculus in HOL. Nordic Journal of Computing, 1(1):50-76, 1994. [ bib ]
[35] Thomas F. Melham. The HOL logic extended with quantification over type variables. Formal Methods in System Design, 3(1-2):7-24, 1994. [ bib | .pdf ]
[36] Thomas F. Melham. The HOL logic extended with quantification over type variables. 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, volume 20 of IFIP Transactions A, pages 3-17. North-Holland, 1993. [ bib ]
[37] Bart Jacobs and Tom Melham. Translating dependent type theory into higher order logic. 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, volume 664 of Lecture Notes in Computer Science, pages 209-229. Springer-Verlag, 1993. [ bib ]
[38] T. F. Melham. A package for inductive relation definitions in HOL. 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. [ bib | .pdf ]
[39] Thomas F. Melham. Using recursive types to reason about hardware in higher order logic. 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. [ bib ]
[40] G. Birtwistle, B. Graham, T. Melham, and R. Schediwy. Hardware verification by formal proof. 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. [ bib ]
[41] Albert Camilleri, Mike Gordon, and Tom Melham. Hardware verification using higher-order logic. 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. [ bib ]
[42] Graham Birtwistle, Jeff Joyce, Breen Liblong, Tom Melham, and Rick Schediwy. Specification and VLSI design. 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. [ bib ]
[43] Breen Liblong, Tom Melham, Graham Birtwistle, and John Kendall. Towards a VLSI design tool system. INFOR: Information Systems and Operational Research, 23(4):389-402, November 1985. [ bib ]
[44] Breen Liblong, Tom Melham, Graham Birtwistle, and John Kendall. Towards a VLSI design tool system. In Leo Gotlieb, editor, Canadian Information Processing Society: SESSION 84: Proceedings, pages 37-42. Canadian Information Processing Society, 1984. [ bib ]
[45] B. Liblong, T. Melham, and G. Birtwistle. Exploiting hierarchies in EDICT. In Proceedings of the 1984 Canadian Conference on VLSI, 1984. [ bib ]

Invited Articles

[46] Ziyad Hanna and Tom Melham. A symbolic execution framework for algorithm-level modelling. In Priyank Kalla and Prabhat Mishra, editors, High Level Design Validation and Test Workshop, 2009. HLDVT 2009., pages 94-99. IEEE, 2009. [ bib | DOI | .pdf ]
[47] Tom Melham. Integrating model checking and theorem proving in a reflective functional language. 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, volume 2999 of Lecture Notes in Computer Science, pages 36-39. Springer-Verlag, 2004. [ bib | .pdf ]
[48] Tom Melham. Abstract: Experience with practical formal verification at an industrial scale. 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. [ bib | .pdf ]
[49] Thomas F. Melham. PROSPER: An investigation into software architecture for embedded proof engines. In Alessandro Armando, editor, Frontiers of Combining Systems: 4th International Workshop, FroCoS 2002: Santa Margherita Ligure, Italy, April 8-10, 2002: Proceedings, volume 2309 of Lecture Notes in Artificial Intelligence, pages 193-206. Springer-Verlag, 2002. [ bib | .pdf ]
[50] Stuart Aitken, Philip Gray, Tom Melham, and Muffy Thomas. Interactive proof discovery: An empirical study of HOL users. 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. [ bib | .pdf ]
[51] T. F. Melham. A mechanized theory of the π-calculus in HOL. 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. [ bib ]
[52] Thomas F. Melham. Abstraction mechanisms for hardware verification. In Michael Yoeli, editor, Formal Verification of Hardware Design, pages 30-49. IEEE Computer Society Press, 1990. [ bib ]
[53] Thomas F. Melham. Automating recursive type definitions in higher order logic. In G. Birtwistle and P. A. Subrahmanyam, editors, Current Trends in Hardware Verification and Automated Theorem Proving, pages 341-386. Springer-Verlag, 1989. [ bib | .pdf ]
[54] Thomas F. Melham. Abstraction mechanisms for hardware verification. In Graham Birtwistle and P. A. Subrahmanyam, editors, VLSI Specification, Verification and Synthesis, volume SECS35 of The Kluwer International Series in Engineeering and Computer Science, pages 267-291. Kluwer Academic Publishers, 1988. [ bib ]

Dissertations

[55] Thomas Frederick Melham. Formalizing Abstraction Mechanisms for Hardware Verification in Higher Order Logic. PhD thesis, University of Cambridge, August 1989. [ bib ]

Edited Works

[56] Joe Hurd and Tom Melham, editors. Theorem Proving in Higher Order Logics: 18th International Conference, TPHOLs 2005: Oxford, UK, August 22-25, 2005: Proceedings, volume 3603 of Lecture Notes in Computer Science. Springer-Verlag, 2005. [ bib | DOI | http ]
[57] Tiziana Margaria and Tom Melham, editors. Correct Hardware Design and Verification Methods: 11th IFIP WG10.5 Advanced Research Working Conference, CHARME 2001: Livingston, Scotland, UK, September 4-7 2001: Proceedings, volume 2144 of Lecture Notes in Computer Science. Springer-Verlag, 2001. [ bib | http ]
[58] 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. [ bib | .pdf ]
[59] Tom Melham and Mary Sheeran, editors. Fifth International Workshop on Designing Correct Circuits: Barcelona, 27-28 March 2004: Participants' Proceedings. ETAPS 2004, March 2004. A Satellite Event of the ETAPS 2004 group of conferences. [ bib | .pdf ]
[60] Mary Sheeran and Tom Melham, editors. Designing Correct Circuits (DCC'02). ETAPS 2002, April 2002. Proceedings of the Workshop on Designing Correct Circuits held during 6-7 April 2002 in Grenoble, France. [ bib ]
[61] Tom Melham. Special issue on theorem provers and functional programming. Journal of Functional Programming, 9(2):i-ii, March 1999. [ bib ]
[62] Thomas F. Melham and Juanito Camilleri, editors. Higher Order Logic Theorem Proving and Its Applications: 7th International Workshop: Valletta, Malta, September 19-22, 1994: Proceedings, volume 859 of Lecture Notes in Computer Science. Springer-Verlag, 1994. [ bib ]
[63] Tom Melham and Juanito Camilleri, editors. Supplementary Proceedings of the 7th International Workshop on Higher Order Logic Theorem Proving and its Applications. University of Malta, September 1994. [ bib ]
[64] M. J. C. Gordon and T. F. Melham, editors. Introduction to HOL: A theorem proving environment for higher order logic. Cambridge University Press, 1993. [ bib | .html ]
[65] V. Stavridou, T. F. Melham, and R. T. Boute, editors. 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, volume 10 of IFIP Transactions A. North-Holland, 1992. [ bib ]

Patents

[66] Thomas F. Melham and Robert B. Jones. Automatic symbolic indexing methods for formal verification on a symbolic lattice domain, June 2004. US Patent 7,310,790. [ bib ]

Research Reports and other Publications

[67] Rajdeep Mukherjee, Peter Schrammel, Leopold Haller, Daniel Kroening, and Tom Melham. Lifting CDCL to template-based abstract domains for program verification. arXiv Computing Research Repository, arXiv:1707.02011 [cs.LO], July 2017. [ bib | http ]
[68] Lihao Liang, Paul E. McKenney, Daniel Kroening, and Tom Melham. Verification of the tree-based hierarchical read-copy update in the linux kernel. arXiv Computing Research Repository, arXiv:1610:03052 [cs.LO], October 2016. [ bib ]
[69] Rajdeep Mukherjee, Saurabh Joshi, Andreas Griesmayer, Daniel Kroening, and Tom Melham. Equivalence checking a floating-point unit against a high-level c model: Extended version. arXiv Computing Research Repository, arXiv:1609.00169 [cs.SE], September 2016. [ bib ]
[70] Clark Barrett, Daniel Kroening, and Tom Melham. Problem solving for the 21st century: Efficient solvers for satisfiability modulo theories. Knowledge Transfer Report 3, London Mathematical Society and the Smith Institute for Industrial Mathematics and System Engineering, June 2014. [ bib ]
[71] Peter Schrammel, Tom Melham, and Daniel Kroening. Chaining test cases for reactive system testing (extended version). arXiv Computing Research Repository, abs/1306.3882, November 2013. [ bib | .pdf ]
[72] Tom Melham, Raphael Cohn, and Ian Childs. On the semantics of reFLect as a basis for a reflective theorem prover. arXiv Computing Research Repository, arXiv:1309.5742 [cs.LO], September 2013. [ bib | .pdf ]
[73] Peter Böhm and Tom Melham. Design and verification of on-chip communication protocols. Research Report RR-08-05, Oxford University Computing Laboratory, April 2008. [ bib | .pdf ]
[74] Peter Böhm and Tom Melham. Design and verification of on-chip communication protocols. 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. [ bib | .pdf ]
[75] Tom Melham and John O'Leary. A functional HDL in reFLect. 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. [ bib | .pdf ]
[76] Jim Grundy, Tom Melham, and John O'Leary. A reflective functional language for hardware design and theorem proving. Research Report PRG-RR-03-16, Programming Research Group, Oxford University Computing Laboratory, October 2003. [ bib | .pdf ]
[77] Mark D. Aagaard, Thomas F. Melham, and John W. O'Leary. Xs are for trajectory evaluation, Booleans are for theorem proving (extended version). Technical Report TR-2000-52, Department of Computing Science, University of Glasgow, January 2000. [ bib | .pdf ]
[78] Kong Woei Susanto and Tom Melham. Formally analysed dynamic synthesis of hardware. 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. [ bib ]
[79] Stuart Aitken, Philip Gray, Tom Melham, and Muffy Thomas. ITP project anthology. Technical Report TR-1997-36, Department of Computing Science, University of Glasgow, November 1997. [ bib ]
[80] Tom F. Melham. Some research issues in higher order logic theorem proving. BRICS Notes Series NS-96-7, Department of Computer Science, University of Aarhus, October 1996. [ bib ]
[81] Stuart Aitken, Philip Gray, Tom Melham, and Muffy Thomas. A study of user activity in interactive theorem proving. 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. [ bib ]
[82] Juanito Camilleri and Tom Melham. Reasoning with inductively defined relations in the HOL theorem prover. Technical Report 265, Computer Laboratory, University of Cambridge, August 1992. [ bib | .pdf ]
[83] T. F. Melham. A mechanized theory of the π-calculus in HOL. Technical Report 244, Computer Laboratory, University of Cambridge, January 1992. [ bib ]
[84] T. F. Melham. The HOL finite_sets Library. Computer Laboratory, University of Cambridge, February 1992. [ bib ]
[85] T. F. Melham. The HOL pred_sets Library. Computer Laboratory, University of Cambridge, February 1992. [ bib ]
[86] T. F. Melham. The HOL sets Library. Computer Laboratory, University of Cambridge, October 1991. [ bib ]
[87] T. F. Melham. The HOL string Library. Computer Laboratory, University of Cambridge, June 1991. [ bib ]
[88] Graham Birtwistle, Brian Graham, Tom Melham, and Rick Schediwy. Hardware verification by formal proof. Research Report 88/328/40, Department of Computer Science, University of Calgary, October 1988. [ bib ]
[89] Thomas F. Melham. Automating recursive type definitions in higher order logic. Technical Report 146, Computer Laboratory, University of Cambridge, September 1988. [ bib ]
[90] Thomas F. Melham. Using recursive types to reason about hardware in higher order logic. Technical Report 135, Computer Laboratory, University of Cambridge, May 1988. [ bib ]
[91] Thomas F. Melham. Abstraction mechanisms for hardware verification. Technical Report 106, Computer Laboratory, University of Cambridge, May 1987. [ bib ]
[92] Albert Camilleri, Mike Gordon, and Tom Melham. Hardware verification using higher-order logic. Technical Report 91, Computer Laboratory, University of Cambridge, June 1986. [ bib ]
[93] Graham Birtwistle, Jeff Joyce, Breen Liblong, Tom Melham, and Rick Schediwy. Specification and VLSI design. Research Report 85/220/33, Department of Computer Science, University of Calgary, November 1985. [ bib ]
[94] Breen Liblong, Tom Melham, Graham Birtwistle, and John Kendall. Towards a VLSI design tool system. Research Report 84/175/33, Department of Computer Science, University of Calgary, November 1984. [ bib ]
[95] Graham Birtwistle, David Hill, John Kendall, Bill Coates, Richard Esau, Wallace Kroeker, Breen Liblong, Erwin Liu, Tom Melham, and Rick Schediwy. EDICT: An environment for design using integrated circuit tools. Research Report 84/155/13, Department of Computer Science, University of Calgary, June 1984. [ bib ]

This file was generated by bibtex2html 1.96.

Tom Melham, last updated Sun 22 Oct 2017 17:39:42 BST