[1]

Tom Melham.
Symbolic trajectory evaluation.
In Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick
Bloem, editors, Handbook of Model Checking, chapter 25, pages 831870.
Springer International Publishing, 2018.
[ bib 
DOI ]

[2]

Sean Heelan, Tom Melham, and Daniel Kroening.
Automatic heap layout manipulation for exploitation.
In William Enck and Adrienne Porter Felt, editors, 27th USENIX
Security Symposium, USENIX Security 18: Baltimore, MD, USA, August 1517,
2018, pages 763779. USENIX Association, 2018.
[ bib 
.pdf ]

[3]

Lihao Liang, Paul E. McKenney, Daniel Kroening, and Tom Melham.
Verification of treebased hierarchical ReadCopy Update in the
Linux kernel.
In Jan Madsen and Ayse K. Coskun, editors, 2018 Design,
Automation & Test in Europe Conference & Exhibition, DATE 2018,
Dresden, Germany, March 1923, 2018, pages 6166. European Design and
Automation Association, 2018.
[ bib 
DOI 
.pdf ]

[4]

Rajdeep Mukherjee, Peter Schrammel, Leopold Haller, Daniel Kroening, and Tom
Melham.
Lifting CDCL to templatebased 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 36, 2017, Proceedings, volume 10482 of
Lecture Notes in Computer Science, pages 307326. Springer, Cham, 2017.
[ bib 
DOI 
.pdf ]

[5]

Lihao Liang, Tom Melham, Daniel Kroening, Peter Schrammel, and Michael
Tautschnig.
Effective verification for lowlevel software with competing
interrupts.
ACM Transactions on Embedded Computing Systems,
17(2):36:136:26, December 2017.
[ bib 
DOI 
.pdf ]

[6]

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 1418, 2016, pages 11521155. European Design and
Automation Association, 2016.
[ bib 
DOI 
.pdf ]

[7]

Rajdeep Mukherjee, Saurabh Joshi, Andreas Griesmayer, Daniel Kroening, and Tom
Melham.
Equivalence checking of a floatingpoint unit against a highlevel
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 911, 2016, Proceedings, volume 9995
of Lecture Notes in Computer Science, pages 551558. SpringerVerlag,
2016.
[ bib 
DOI ]

[8]

Peter Schrammel, Tom Melham, and Daniel Kroening.
Generating test case chains for reactive systems.
International Journal on Software Tools for Technology
Transfer, 18(3):319334, June 2016.
[ bib 
DOI 
.pdf ]

[9]

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 810, 2015, pages 712. IEEE
Computer Society, 2015.
[ bib 
DOI ]

[10]

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 810, 2015, pages 1318. IEEE
Computer Society, 2015.
[ bib 
DOI ]

[11]

Daniel Kroening, Lihao Liang, Tom Melham, Peter Schrammel, and Michael
Tautschnig.
Effective verification of lowlevel 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 913, 2015, pages 229234. EDA
Consortium, 2015.
[ bib 
.pdf ]

[12]

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 1315,
2013, Proceedings, volume 8254 of Lecture Notes in Computer Science,
pages 133148. Springer Verlag, November 2013.
[ bib 
DOI 
.pdf ]

[13]

Alex Horn, Michael Tautschnig, Celina Val, Lihao Liang, Tom Melham, Jim Grundy,
and Daniel Kroening.
Formal covalidation of lowlevel hardware/software interfaces.
In Barbara Jobstmann and Sandip Ray, editors, FMCAD 2013:
Formal Methods in ComputerAided Design: Portland, Oregon, USA, 2023
October 2013, pages 121128. IEEE, 2013.
[ bib 
DOI 
.pdf ]

[14]

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 ComputerAided Design: Portland, Oregon, USA,
2023 October 2013, pages 97104. IEEE, 2013.
[ bib 
DOI 
.pdf ]

[15]

Tom Melham.
Modelling, abstraction, and computation in systems biology: A view
from computer science.
Progress in Biophysics and Molecular Biology,
111(23):129136, April 2013.
Focussed Issue: Conceptual Foundations of Systems Biology.
[ bib 
DOI ]

[16]

Zurab Khasidashvili, Gavriel Gavrielov, and Tom Melham.
Assumeguarantee validation for STE properties within an SVA
environment.
In Armin Biere and Carl Pixley, editors, Proceedings of 9th
International Conference: 2009 Formal Methods in ComputerAided Design:
FMCAD 2009, pages 108115. IEEE, 2009.
[ bib 
DOI 
.pdf ]

[17]

Ziyad Hanna and Tom Melham.
A symbolic execution framework for algorithmlevel modelling.
In Priyank Kalla and Prabhat Mishra, editors, High Level Design
Validation and Test Workshop, 2009. HLDVT 2009., pages 9499. IEEE, 2009.
[ bib 
DOI 
.pdf ]

[18]

Peter Böhm and Tom Melham.
A refinement approach to design and verification of onchip
communication protocols.
In Alessandro Cimatti and Robert B. Jones, editors, 2008 Formal
Methods in Computer Aided Design: Portland, Oregon, USA: 1720
November 2008, pages 136143. IEEE, 2008.
[ bib 
DOI 
.pdf ]

[19]

Peter Böhm and Tom Melham.
Design and verification of onchip communication protocols.
In Gordon J. Pace and Satnam Singh, editors, Seventh
International Workshop on Designing Correct Circuits: Budapest,
2930 March 2008: Participants' Proceedings, pages 1529. ETAPS 2008,
March 2008.
A Satellite Event of the ETAPS 2008 group of conferences.
[ bib 
.pdf ]

[20]

Sara Adams, Magnus Björk, Tom Melham, and CarlJohan Seger.
Automatic abstraction in symbolic trajectory evaluation.
In Jason Baumgartner and Mary Sheeran, editors, Formal Methods
in Computer Aided Design: FMCAD 2007: November 1114 2007, Austin,
Texas, USA, pages 127135. IEEE Computer Society, 2007.
[ bib 
DOI 
.pdf ]

[21]

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 ]

[22]

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, 2526 March 2006:
Participants' Proceedings. ETAPS 2006, March 2006.
A Satellite Event of the ETAPS 2006 group of conferences.
[ bib 
.pdf ]

[23]

Mary Sheeran and Tom Melham, editors.
Sixth International Workshop on Designing Correct
Circuits: Vienna, 2526 March 2006: Participants' Proceedings. ETAPS
2006, March 2006.
A Satellite Event of the ETAPS 2006 group of conferences.
[ bib 
.pdf ]

[24]

Jim Grundy, Tom Melham, and John O'Leary.
A reflective functional language for hardware design and theorem
proving.
Journal of Functional Programming, 16(2):157196, March 2006.
[ bib 
DOI 
.pdf ]

[25]

Jim Grundy, Tom Melham, Sava Krstić, and Sean McLaughlin.
Tool building requirements for an API to firstorder solvers.
Electronic Notes in Theoretical Computer Science,
144(2):1526, January 2006.
[ bib 
DOI 
.pdf ]

[26]

CarlJohan 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 ComputerAided Design of Integrated
Circuits and Systems, 24(9):13811405, September 2005.
[ bib 
DOI 
.pdf ]

[27]

Joe Hurd and Tom Melham, editors.
Theorem Proving in Higher Order Logics: 18th International
Conference, TPHOLs 2005: Oxford, UK, August 2225, 2005:
Proceedings, volume 3603 of Lecture Notes in Computer Science.
SpringerVerlag, 2005.
[ bib 
DOI 
http ]

[28]

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 47, 2004: Proceedings, volume 2999 of
Lecture Notes in Computer Science, pages 3639. SpringerVerlag, 2004.
[ bib 
.pdf ]

[29]

Tom Melham and Mary Sheeran, editors.
Fifth International Workshop on Designing Correct
Circuits: Barcelona, 2728 March 2004: Participants' Proceedings.
ETAPS 2004, March 2004.
A Satellite Event of the ETAPS 2004 group of conferences.
[ bib 
.pdf ]

[30]

Kong Woei Susanto and Tom Melham.
An AMBAARM7 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 57, 2003: Proceedings,
volume 2885 of Lecture Notes in Computer Science, pages 4867.
SpringerVerlag, 2003.
[ bib 
.pdf ]

[31]

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: 15th16th
April 2003: Liverpool, pages 12. Department of Computer Science,
University of Liverpool, 2003.
[ bib 
.pdf ]

[32]

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):189210, February 2003.
[ bib 
DOI 
http ]

[33]

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 ComputerAided Design: 4th International Conference, FMCAD 2002:
Portland, OR, USA, November 68, 2002: Proceedings, volume 2517
of Lecture Notes in Computer Science, pages 118. SpringerVerlag,
2002.
[ bib 
DOI 
.pdf ]

[34]

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 810, 2002: Proceedings, volume 2309 of Lecture Notes
in Artificial Intelligence, pages 193206. SpringerVerlag, 2002.
[ bib 
.pdf ]

[35]

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 67 April 2002 in Grenoble, France.
[ bib ]

[36]

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 47 2001: Proceedings, volume 2144 of
Lecture Notes in Computer Science. SpringerVerlag, 2001.
[ bib 
http ]

[37]

Robert B. Jones, John W. O'Leary, CarlJohan H. Seger, Mark D. Aagaard, and
Thomas F. Melham.
Practical formal verification in microprocessor design.
IEEE Design & Test of Computers, 18(4):1625, July/August
2001.
[ bib 
DOI 
.pdf ]

[38]

Kong Woei Susanto and Tom Melham.
Formally analyzed dynamic synthesis of hardware.
The Journal of Supercomputing, 19(1):722, May 2001.
[ bib 
DOI 
.ps ]

[39]

Mark D. Aagaard, Robert B. Jones, Thomas F. Melham, John W. O'Leary, and
CarlJohan H. Seger.
A methodology for largescale hardware verification.
In Warren A. Hunt, Jr. and Steven D. Johnson, editors, Formal
Methods in ComputerAided Design: Third International Conference, FMCAD
2000: Austin, TX, USA, November 13, 2000: Proceedings, volume
1954 of Lecture Notes in Computer Science, pages 263282.
SpringerVerlag, 2000.
[ bib 
.pdf ]

[40]

S. Aitken and T. Melham.
An analysis of errors in interactive proof attempts.
Interacting with Computers, 12(6):565586, June 2000.
[ bib ]

[41]

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 7892. SpringerVerlag, 2000.
[ bib 
.pdf ]

[42]

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
2729, 1999: Proceedings, volume 1703 of Lecture Notes in Computer
Science, pages 202218. SpringerVerlag, 1999.
[ bib 
.pdf ]

[43]

Tom Melham.
Special issue on theorem provers and functional programming.
Journal of Functional Programming, 9(2):iii, March 1999.
[ bib ]

[44]

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 105117. Australian National University, 1998.
[ bib ]

[45]

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 1517,
1998, Napa Valley, California, pages 308309. IEEE Computer Society,
1998.
[ bib 
.pdf ]

[46]

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):263284, February 1998.
[ bib ]

[47]

Andrew D. Gordon and Tom Melham.
Five axioms of alphaconversion.
In J. von Wright, J. Grundy, and J. Harrison, editors, Theorem
Proving in Higher Order Logics: 9th International Conference, TPHOLs'96:
Turku, Finland, August 2630, 1996: Proceedings, volume 1125 of
Lecture Notes in Computer Science, pages 173190. SpringerVerlag, 1996.
[ bib 
.pdf ]

[48]

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 18.
University of York, 1996.
[ bib ]

[49]

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 ]

[50]

Thomas F. Melham and Juanito Camilleri, editors.
Higher Order Logic Theorem Proving and Its Applications: 7th
International Workshop: Valletta, Malta, September 1922, 1994:
Proceedings, volume 859 of Lecture Notes in Computer Science.
SpringerVerlag, 1994.
[ bib ]

[51]

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 ]

[52]

T. F. Melham.
A mechanized theory of the Πcalculus in HOL.
Nordic Journal of Computing, 1(1):5076, 1994.
[ bib ]

[53]

Thomas F. Melham.
The HOL logic extended with quantification over type variables.
Formal Methods in System Design, 3(12):724, 1994.
[ bib 
.pdf ]

[54]

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, 2124 September
1992, volume 20 of IFIP Transactions A, pages 317. NorthHolland,
1993.
[ bib ]

[55]

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, 1618, 1993, Utrecht, The
Netherlands: Proceedings, volume 664 of Lecture Notes in Computer
Science, pages 209229. SpringerVerlag, 1993.
[ bib ]

[56]

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 ]

[57]

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

[58]

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 2830, 1991, pages 350357. IEEE Computer Society Press, 1992.
[ bib 
.pdf ]

[59]

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,
2224 June 1992, volume 10 of IFIP Transactions A. NorthHolland,
1992.
[ bib ]

[60]

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 219237. University of Edinburgh,
1991.
Preliminary proceedings, published electronically after the workshop.
[ bib ]

[61]

Thomas F. Melham.
Abstraction mechanisms for hardware verification.
In Michael Yoeli, editor, Formal Verification of Hardware
Design, pages 3049. IEEE Computer Society Press, 1990.
[ bib ]

[62]

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

[63]

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 341386.
SpringerVerlag, 1989.
[ bib 
.pdf ]

[64]

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 267291.
Kluwer Academic Publishers, 1988.
[ bib ]

[65]

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, 46
July, 1988, pages 2750. NorthHolland, 1988.
[ bib ]

[66]

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 379384. Canadian Society for Electrical Engineering, 1988.
[ bib ]

[67]

Albert Camilleri, Mike Gordon, and Tom Melham.
Hardware verification using higherorder 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, 911 September, 1986, pages 4367.
NorthHolland, 1987.
[ bib ]

[68]

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 8397. NorthHolland, 1986.
[ bib ]

[69]

Breen Liblong, Tom Melham, Graham Birtwistle, and John Kendall.
Towards a VLSI design tool system.
INFOR: Information Systems and Operational Research,
23(4):389402, November 1985.
[ bib ]

[70]

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 3742. Canadian Information
Processing Society, 1984.
[ bib ]

[71]

B. Liblong, T. Melham, and G. Birtwistle.
Exploiting hierarchies in EDICT.
In Proceedings of the 1984 Canadian Conference on VLSI,
1984.
[ bib ]
