|
[1]
|
Natasha Yogananda Jeppu, Tom Melham, and Daniel Kroening.
Enhancing active model learning with equivalence checking using
simulation relations.
Formal Methods in System Design, August 2023.
[ bib |
DOI |
.pdf ]
|
|
[2]
|
Seung Hoon Park, Rekha Pai, and Tom Melham.
A formal CHERI-C semantics for verification.
In Sriram Sankaranarayanan and Natasha Sharygina, editors, Tools
and Algorithms for the Construction and Analysis of Systems: TACAS 2023,
volume 13993 of Lecture Notes in Computer Science, pages 549-568.
Springer, Cham, 2023.
[ bib |
DOI |
.pdf ]
|
|
[3]
|
Natasha Yogananda Jeppu, Tom Melham, and Daniel Kroening.
Active learning of abstract system models from traces using model
checking.
In Cristiana Bolchini, Ingrid Verbauwhede, and Ioana Vatajelu,
editors, 2022 Design, Automation & Test in Europe Conference &
Exhibition, DATE 2022, Antwerp, Belgium, March 14-23, 2022, pages
100-103. IEEE, March 2022.
[ bib |
DOI |
.pdf ]
|
|
[4]
|
Kaled M. Alshmrany, Ahmed Bhayat, Franz Brauße, Lucas C. Cordeiro,
Konstantin Korovin, Tom Melham, Mustafa A. Mustafa, Pierre Olivier, Giles
Reger, and Fedor Shmarov.
Position paper: Towards a hybrid approach to protect against memory
safety vulnerabilities.
In IEEE Secure Development Conference, SecDev 2022, Atlanta,
GA, USA, October 18-20, 2022, pages 52-58. IEEE, 2022.
[ bib |
DOI ]
|
|
[5]
|
Dapeng Gao and Tom Melham.
End-to-end formal verification of a RISC-V processor extended with
capability pointers.
In Ruzica Piskac and Michael W. Whalen, editors, Proceedings of
the 21st Conference on Formal Methods in Computer-Aided Design –- FMCAD
2021, volume 2, pages 24-33. TUI Wien Academic Press, October 2021.
[ bib |
DOI |
.pdf ]
|
|
[6]
|
Isaac Dunn, Hadrien Pouget, Daniel Kroening, and Tom Melham.
Exposing previously undetectable faults in deep neural networks.
In Cristian Cadar and Xiangyu Zhang, editors, ISSTA 2021:
Proceedings of the 30th ACM SIGSOFT International Symposium on Software
Testing and Analysis, pages 56-66. Association for Computing Machinery,
2021.
[ bib |
DOI |
.pdf ]
|
|
[7]
|
Mohammadhosein Hasanbeig, Natasha Yogananda Jeppu, Alessandro Abate, Tom
Melham, and Daniel Kroening.
DeepSynth: Automata synthesis for automatic task segmentation in
deep reinforcement learning.
In Thirty-Fifth AAAI Conference on Artificial Intelligence,
AAAI 2021, Thirty-Third Conference on Innovative Applications of Artificial
Intelligence, IAAI 2021, The Eleventh Symposium on Educational Advances in
Artificial Intelligence, EAAI 2021, Virtual Event, February 2-9, 2021,
pages 7647-7656. AAAI Press, 2021.
[ bib |
http ]
|
|
[8]
|
Bertie Vidgen, Sam Staton, Scott Hale, Ohad Kammar, Helen Margetts, Tom Melham,
and Marcin Szymczak.
Recalibrating classifiers for interpretable abusive content
detection.
In Proceedings of the Fourth Workshop on Natural Language
Processing and Computational Social Science, pages 132-138. Association for
Computational Linguistics, November 2020.
[ bib |
DOI |
http ]
|
|
[9]
|
Natasha Yogananda Jeppu, Thomas Melham, Daniel Kroening, and John O'Leary.
Learning concise models from long execution traces.
In 57th ACM/IEEE Design Automation Conference, DAC 2020, San
Francisco, CA, USA, July 20-24, 2020, pages 1-6. IEEE Press, 2020.
[ bib |
DOI ]
|
|
[10]
|
Sean Heelan, Tom Melham, and Daniel Kroening.
Gollum: Modular and greybox exploit generation for heap overflows in
interpreters.
In Lorenzo Cavallaro, Johannes Kinder, XiaoFeng Wang, and Jonathan
Katz, editors, Proceedings of the 2019 ACM SIGSAC Conference on
Computer and Communications Security, CCS 2019, London, UK, November 11-15,
2019, pages 1689-1706. ACM, 2019.
[ bib |
DOI |
.pdf ]
|
|
[11]
|
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 831-870.
Springer International Publishing, 2018.
[ bib |
DOI ]
|
|
[12]
|
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 15-17,
2018, pages 763-779. USENIX Association, 2018.
[ bib |
.pdf ]
|
|
[13]
|
Lihao Liang, Paul E. McKenney, Daniel Kroening, and Tom Melham.
Verification of tree-based hierarchical Read-Copy 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 19-23, 2018, pages 61-66. European Design and
Automation Association, 2018.
[ bib |
DOI |
.pdf ]
|
|
[14]
|
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 ]
|
|
[15]
|
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,
17(2):36:1-36:26, December 2017.
[ bib |
DOI |
.pdf ]
|
|
[16]
|
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 ]
|
|
[17]
|
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 ]
|
|
[18]
|
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 ]
|
|
[19]
|
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 ]
|
|
[20]
|
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 ]
|
|
[21]
|
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 ]
|
|
[22]
|
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 ]
|
|
[23]
|
Alex Horn, Michael Tautschnig, Celina Val, Lihao 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 |
DOI |
.pdf ]
|
|
[24]
|
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 |
DOI |
.pdf ]
|
|
[25]
|
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 ]
|
|
[26]
|
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 ]
|
|
[27]
|
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 ]
|
|
[28]
|
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 ]
|
|
[29]
|
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 ]
|
|
[30]
|
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 ]
|
|
[31]
|
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 ]
|
|
[32]
|
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 ]
|
|
[33]
|
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 ]
|
|
[34]
|
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 ]
|
|
[35]
|
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 ]
|
|
[36]
|
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 ]
|
|
[37]
|
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 ]
|
|
[38]
|
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 ]
|
|
[39]
|
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 ]
|
|
[40]
|
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 ]
|
|
[41]
|
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 ]
|
|
[42]
|
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 ]
|
|
[43]
|
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 |
DOI |
.pdf ]
|
|
[44]
|
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 ]
|
|
[45]
|
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 ]
|
|
[46]
|
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 ]
|
|
[47]
|
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 ]
|
|
[48]
|
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 ]
|
|
[49]
|
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 ]
|
|
[50]
|
S. Aitken and T. Melham.
An analysis of errors in interactive proof attempts.
Interacting with Computers, 12(6):565-586, June 2000.
[ bib ]
|
|
[51]
|
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 ]
|
|
[52]
|
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 ]
|
|
[53]
|
Tom Melham.
Special issue on theorem provers and functional programming.
Journal of Functional Programming, 9(2):i-ii, March 1999.
[ bib ]
|
|
[54]
|
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 ]
|
|
[55]
|
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 ]
|
|
[56]
|
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 ]
|
|
[57]
|
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 ]
|
|
[58]
|
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 ]
|
|
[59]
|
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 ]
|
|
[60]
|
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 ]
|
|
[61]
|
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 ]
|
|
[62]
|
T. F. Melham.
A mechanized theory of the Π-calculus in HOL.
Nordic Journal of Computing, 1(1):50-76, 1994.
[ bib ]
|
|
[63]
|
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 ]
|
|
[64]
|
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 ]
|
|
[65]
|
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 ]
|
|
[66]
|
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 ]
|
|
[67]
|
T. Melham.
Higher Order Logic and Hardware Verification, volume 31 of
Cambridge Tracts in Theoretical Computer Science.
Cambridge University Press, 1993.
[ bib |
DOI |
.html ]
|
|
[68]
|
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 ]
|
|
[69]
|
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 ]
|
|
[70]
|
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 ]
|
|
[71]
|
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 ]
|
|
[72]
|
Thomas Frederick Melham.
Formalizing Abstraction Mechanisms for Hardware Verification in
Higher Order Logic.
PhD thesis, University of Cambridge, August 1989.
[ bib ]
|
|
[73]
|
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 ]
|
|
[74]
|
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 ]
|
|
[75]
|
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 ]
|
|
[76]
|
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 ]
|
|
[77]
|
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 ]
|
|
[78]
|
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 ]
|
|
[79]
|
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 ]
|
|
[80]
|
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 ]
|
|
[81]
|
B. Liblong, T. Melham, and G. Birtwistle.
Exploiting hierarchies in EDICT.
In Proceedings of the 1984 Canadian Conference on VLSI,
1984.
[ bib ]
|
|
[82]
|
Seung Hoon Park, Rekha Pai, and Tom Melham.
A formal CHERI-C semantics for verification.
arXiv Computing Research Repository, arXiv:2211.07511 [cs.LO],
January 2023.
[ bib |
http ]
|
|
[83]
|
Natasha Yogananda Jeppu, Tom Melham, and Daniel Kroening.
Active learning of abstract system models from traces using model
checking [extended].
arXiv Computing Research Repository, arXiv:2112.05990 [cs.FL],
December 2021.
[ bib |
http ]
|
|
[84]
|
Isaac Dunn, Hadrien Pouget, Daniel Kroening, and Tom Melham.
Exposing previously undetectable faults in deep neural networks.
arXiv Computing Research Repository, arXiv:2106.00576 [cs.LG],
June 2021.
[ bib |
http ]
|
|
[85]
|
Kaled Alshmrany, Ahmed Bhayat, Lucas Cordeiro, Konstantin Korovin, Tom Melham,
Mustafa A. Mustafa, Pierre Olivier, Giles Reger, and Fedor Shmarov.
Towards a hybrid approach to protect against memory safety
vulnerabilities.
TechRxiv, 2021.
Preprint.
[ bib |
http ]
|
|
[86]
|
Rebecca Williams and Thomas Melham.
Automated decision-making in the public sector.
Practical Law Public Sector, December 2020.
Resource ID w 028 6934.
[ bib |
.pdf ]
|
|
[87]
|
Isaac Dunn, Laura Hanu, Hadrien Pouget, Daniel Kroening, and Tom Melham.
Evaluating robustness to context-sensitive feature perturbations of
different granularities.
arXiv Computing Research Repository, arXiv:2001.11055 [cs.CV],
June 2020.
[ bib |
http ]
|
|
[88]
|
Natasha Yogananda Jeppu, Tom Melham, Daniel Kroening, and John O'Leary.
Learning concise models from long execution traces.
arXiv Computing Research Repository, arXiv:2001.05230 [cs.FL],
January 2020.
[ bib |
http ]
|
|
[89]
|
Rajdeep Mukherjee, Saurahb Joshi, John O'Leary, Daniel Kroening, and Tom
Melham.
Hardware/software co-verification using path-based symbolic
execution.
arXiv Computing Research Repository, arXiv:2001.01324 [cs.FL],
January 2020.
[ bib |
http ]
|
|
[90]
|
Mohammadhosein Hasanbeig, Natasha Yogananda Jeppu, Alessandro Abate, Tom
Melham, and Daniel Kroening.
DeepSynth: Program synthesis for automatic task segmentation in
deep reinforcement learning.
arXiv Computing Research Repository, arXiv:1911.10244 [cs.LG],
November 2019.
[ bib |
http ]
|
|
[91]
|
Andreas Tiemeyer, Tom Melham, Daniel Kroening, and John O'Leary.
CREST: Hardware formal verification with ANSI-C reference
specifications.
arXiv Computing Research Repository, arXiv:1908.01324 [cs.PL],
August 2019.
[ bib |
http ]
|
|
[92]
|
Isaac Dunn, Hadrien Pouget, Tom Melham, and Daniel Kroening.
Adaptive generation of unrestricted adversarial inputs.
arXiv Computing Research Repository, arXiv:1905.02463 [cs.LG],
October 2019.
[ bib |
http ]
|
|
[93]
|
Sean Heelan, Tom Melham, and Daniel Kroening.
Automatic heap layout manipulation for exploitation.
arXiv Computing Research Repository, arXiv:1804.08470 [cs.CR],
April 2018.
[ bib |
http ]
|
|
[94]
|
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 ]
|
|
[95]
|
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 ]
|
|
[96]
|
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 ]
|
|
[97]
|
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 ]
|
|
[98]
|
Peter Schrammel, Tom Melham, and Daniel Kroening.
Chaining test cases for reactive system testing (extended version).
arXiv Computing Research Repository, arXiv:1306.3882 [cs.SE],
November 2013.
[ bib |
http ]
|
|
[99]
|
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 |
http ]
|
|
[100]
|
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 ]
|
|
[101]
|
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 ]
|
|
[102]
|
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 ]
|
|
[103]
|
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 ]
|
|
[104]
|
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 ]
|
|
[105]
|
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 ]
|
|
[106]
|
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 ]
|
|
[107]
|
T. F. Melham.
A mechanized theory of the π-calculus in HOL.
Technical Report 244, Computer Laboratory, University of Cambridge,
January 1992.
[ bib ]
|
|
[108]
|
T. F. Melham.
The HOL finite_sets Library.
Computer Laboratory, University of Cambridge, February 1992.
[ bib ]
|
|
[109]
|
T. F. Melham.
The HOL pred_sets Library.
Computer Laboratory, University of Cambridge, February 1992.
[ bib ]
|
|
[110]
|
T. F. Melham.
The HOL sets Library.
Computer Laboratory, University of Cambridge, October 1991.
[ bib ]
|
|
[111]
|
T. F. Melham.
The HOL string Library.
Computer Laboratory, University of Cambridge, June 1991.
[ bib ]
|
|
[112]
|
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 ]
|
|
[113]
|
Thomas F. Melham.
Automating recursive type definitions in higher order logic.
Technical Report 146, Computer Laboratory, University of Cambridge,
September 1988.
[ bib ]
|
|
[114]
|
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 ]
|
|
[115]
|
Thomas F. Melham.
Abstraction mechanisms for hardware verification.
Technical Report 106, Computer Laboratory, University of Cambridge,
May 1987.
[ bib ]
|
|
[116]
|
Albert Camilleri, Mike Gordon, and Tom Melham.
Hardware verification using higher-order logic.
Technical Report 91, Computer Laboratory, University of Cambridge,
June 1986.
[ bib ]
|
|
[117]
|
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 ]
|
|
[118]
|
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 ]
|
|
[119]
|
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 ]
|