@comment{{Scientific Publications}}

@inproceedings{Gao:2021:EFV, author = {Dapeng Gao and Tom Melham}, title = {End-to-End Formal Verification of a {RISC-V} Processor Extended with Capability Pointers}, booktitle = {Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design –- {FMCAD} 2021}, editor = {Ruzica Piskac and Michael W.~Whalen}, year = {2021}, month = {October}, doi = {10.34727/2021/isbn.978-3-85448-046-4_10}, volume = {2}, pages = {24--33}, publisher = {TUI Wien Academic Press}, url = {http://www.cs.ox.ac.uk/tom.melham/pub/Gao-2021-EFVG.pdf} }

@inproceedings{Dunn:2021:EPU, author = {Isaac Dunn and Hadrien Pouget and Daniel Kroening and Tom Melham}, title = {Exposing Previously Undetectable Faults in Deep Neural Networks}, booktitle = {{ISSTA} 2021: Proceedings of the 30th {ACM} {SIGSOFT} International Symposium on Software Testing and Analysis}, editor = {Cristian Cadar and Xiangyu Zhang}, publisher = {Association for Computing Machinery}, pages = {56--66}, year = {2021}, url = {http://www.cs.ox.ac.uk/tom.melham/pub/Dunn-2021-EPU.pdf}, doi = {10.1145/3460319.3464801} }

@inproceedings{Hasanbeig:2021:DAS, author = {Mohammadhosein Hasanbeig and Natasha Yogananda Jeppu and Alessandro Abate and Tom Melham and Daniel Kroening}, title = {{DeepSynth}: Automata Synthesis for Automatic Task Segmentation in Deep Reinforcement Learning}, booktitle = {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}, publisher = {{AAAI} Press}, year = {2021} }

@inproceedings{Vidgen:2020:RCI, author = {Bertie Vidgen and Sam Staton and Scott Hale and Ohad Kammar and Helen Margetts and Tom Melham and Marcin Szymczak}, title = {Recalibrating classifiers for interpretable abusive content detection}, booktitle = {Proceedings of the Fourth Workshop on Natural Language Processing and Computational Social Science}, month = {November}, year = {2020}, publisher = {Association for Computational Linguistics}, url = {https://www.aclweb.org/anthology/2020.nlpcss-1.14}, doi = {10.18653/v1/2020.nlpcss-1.14}, pages = {132--138} }

@inproceedings{Jeppu:2020:LCMa, author = {Natasha Yogananda Jeppu and Thomas Melham and Daniel Kroening and John O'Leary}, title = {Learning Concise Models from Long Execution Traces}, booktitle = {57th {ACM/IEEE} Design Automation Conference, {DAC} 2020, San Francisco, {CA}, {USA}, July 20--24, 2020}, year = {2020}, publisher = {IEEE Press}, articleno = {92}, pages = {1--6}, doi = {10.1109/DAC18072.2020.9218613} }

@inproceedings{Heelan:2019:GMG, author = {Sean Heelan and Tom Melham and Daniel Kroening}, title = {Gollum: Modular and Greybox Exploit Generation for Heap Overflows in Interpreters}, booktitle = {Proceedings of the 2019 {ACM} {SIGSAC} Conference on Computer and Communications Security, {CCS} 2019, London, UK, November 11-15, 2019}, editor = {Lorenzo Cavallaro and Johannes Kinder and XiaoFeng Wang and Jonathan Katz}, year = {2019}, pages = {1689--1706}, publisher = {ACM}, doi = {10.1145/3319535.3354224}, url = {http://www.cs.ox.ac.uk/tom.melham/pub/Heelan-2019-GMG.pdf} }

@incollection{Melham:2018:STE, author = {Tom Melham}, title = {Symbolic Trajectory Evaluation}, editor = {Edmund M. Clarke and Thomas A. Henzinger and Helmut Veith and Roderick Bloem}, booktitle = {Handbook of Model Checking}, publisher = {Springer International Publishing}, year = {2018}, pages = {831--870}, chapter = {25}, isbn = {978-3-319-10574-1}, eisbn = {978-3-319-10575-8}, doi = {10.1007/978-3-319-10575-8_25} }

@inproceedings{Heelan:2018:AHL, author = {Sean Heelan and Tom Melham and Daniel Kroening}, title = {Automatic Heap Layout Manipulation for Exploitation}, booktitle = {27th {USENIX} Security Symposium, {USENIX} Security 18: Baltimore, MD, USA, August 15--17, 2018}, editor = {William Enck and Adrienne Porter Felt}, isbn = {978-1-931971-46-1}, year = {2018}, pages = {763--779}, publisher = {{USENIX} Association}, url = {http://www.cs.ox.ac.uk/tom.melham/pub/Heelan-2018-AHL.pdf} }

@inproceedings{Liang:2018:VTB, author = {Lihao Liang and Paul E. McKenney and Daniel Kroening and Tom Melham}, title = {Verification of Tree-Based Hierarchical {Read-Copy Update} in the {Linux} Kernel}, booktitle = {2018 Design, Automation {\&} Test in Europe Conference {\&} Exhibition, {DATE} 2018, Dresden, Germany, March 19--23, 2018}, editor = {Jan Madsen and Ayse K. Coskun}, pages = {61--66}, year = {2018}, publisher = {European Design and Automation Association}, doi = {10.23919/DATE.2018.8341980}, isbn = {978-3-9819263-1-6}, issn = {1558-1101}, url = {http://www.cs.ox.ac.uk/tom.melham/pub/Liang-2018-VTB.pdf} }

@inproceedings{Mukherjee:2017:LCT, author = {Rajdeep Mukherjee and Peter Schrammel and Leopold Haller and Daniel Kroening and Tom Melham}, title = {Lifting {CDCL} to Template-Based Abstract Domains for Program Verification}, booktitle = {Automated Technology for Verification and Analysis: 15th International Symposium, ATVA 2017, Pune, India, October 3-6, 2017, Proceedings}, editor = {Deepak D'Souza and K. Narayan Kumar}, series = {Lecture Notes in Computer Science}, volume = {10482}, pages = {307--326}, year = {2017}, publisher = {Springer, Cham}, issn = {0302-9743}, doi = {10.1007/978-3-319-68167-2_21}, isbn = {978-3-319-68166-5}, url = {http://www.cs.ox.ac.uk/tom.melham/pub/Mukherjee-2017-LCT.pdf} }

@article{Liang:2017:EVL, author = {Lihao Liang and Tom Melham and Daniel Kroening and Peter Schrammel and Michael Tautschnig}, title = {Effective Verification for Low-Level Software with Competing Interrupts}, journal = {ACM Transactions on Embedded Computing Systems}, volume = {17}, number = {2}, month = {December}, year = {2017}, pages = {36:1--36:26}, doi = {10.1145/3147432}, publisher = {ACM}, issn = {1539-9087}, url = {http://www.cs.ox.ac.uk/tom.melham/pub/Liang-2017-EVL.pdf} }

@inproceedings{Mukherjee:2016:USV, author = {Rajdeep Mukherjee and Peter Schrammel and Daniel Kroening and Tom Melham}, title = {Unbounded safety verification for hardware using software analyzers}, booktitle = {2016 Design, Automation {\&} Test in Europe Conference {\&} Exhibition, {DATE} 2016, Dresden, Germany, March 14--18, 2016}, editor = {Luca Fanucci and J{\"{u}}rgen Teich}, pages = {1152--1155}, year = {2016}, publisher = {European Design and Automation Association}, isbn = {978-3-9815370-6-2}, issn = {1558-1101}, doi = {10.3850/9783981537079_0274}, url = {http://www.cs.ox.ac.uk/tom.melham/pub/Mukherjee-2016-USV.pdf} }

@inproceedings{Mukherjee:2016:ECF, author = {Rajdeep Mukherjee and Saurabh Joshi and Andreas Griesmayer and Daniel Kroening and Tom Melham}, title = {Equivalence Checking of a Floating-Point Unit Against a High-Level {C} Model}, booktitle = {{FM} 2016: Formal Methods - 21st International Symposium, Limassol, Cyprus, November 9-11, 2016, Proceedings}, editor = {John S. Fitzgerald and Constance L. Heitmeyer and Stefania Gnesi and Anna Philippou}, series = {Lecture Notes in Computer Science}, volume = {9995}, pages = {551--558}, year = {2016}, publisher = {Springer-Verlag}, issn = {0302-9743}, doi = {10.1007/978-3-319-48989-6_33}, isbn = {978-3-319-48988-9} }

@article{Schrammel:GTC:2016, author = {Peter Schrammel and Tom Melham and Daniel Kroening}, title = {Generating test case chains for reactive systems}, journal = {International Journal on Software Tools for Technology Transfer}, year = {2016}, volume = {18}, number = {3}, month = {June}, pages = {319--334}, issn = {1433-2779}, doi = {10.1007/s10009-014-0358-6}, url = {http://www.cs.ox.ac.uk/tom.melham/pub/Schrammel-2016-GTC.pdf} }

@inproceedings{Mukherjee:2015:HVU, author = {Rajdeep Mukherjee and Daniel Kroening and Tom Melham}, title = {Hardware Verification Using Software Analyzers}, booktitle = {2015 {IEEE} Computer Society Annual Symposium on VLSI, {ISVLSI} 2015, Montpellier, France, July 8-10, 2015}, pages = {7--12}, year = {2015}, publisher = {{IEEE} Computer Society}, doi = {10.1109/ISVLSI.2015.107} }

@inproceedings{Mukherjee:2015:ECU, author = {Rajdeep Mukherjee and Daniel Kroening and Tom Melham and Mandayam K. Srivas}, title = {Equivalence Checking Using Trace Partitioning}, booktitle = {2015 {IEEE} Computer Society Annual Symposium on VLSI, {ISVLSI} 2015, Montpellier, France, July 8-10, 2015}, pages = {13--18}, year = {2015}, publisher = {{IEEE} Computer Society}, doi = {10.1109/ISVLSI.2015.110} }

@inproceedings{Kroening:2015:EVL, author = {Daniel Kroening and Lihao Liang and Tom Melham and Peter Schrammel and Michael Tautschnig}, title = {Effective Verification of Low-Level Software with Nested Interrupts}, booktitle = {Proceedings of the 2015 Design, Automation {\&} Test in Europe Conference {\&} Exhibition, {DATE} 2015, Grenoble, France, March 9-13, 2015}, editor = {Wolfgang Nebel and David Atienza}, year = {2015}, pages = {229--234}, isbn = {978-3-9815370-4-8}, publisher = {{EDA Consortium}}, url = {http://www.cs.ox.ac.uk/tom.melham/pub/Kroening-2015-EVL.pdf} }

@inproceedings{Schrammel:2013:CTC, author = {Peter Schrammel and Tom Melham and Daniel Kroening}, title = {Chaining Test Cases for Reactive System Testing}, booktitle = {Testing Software and Systems - 25th {IFIP} {WG} 6.1 International Conference, {ICTSS} 2013, Istanbul, Turkey, November 13-15, 2013, Proceedings}, editor = {H\"{u}sn\"{u} Yenig\"{u}n and Cemal Yilmaz and Andreas Ulrich}, pages = {133--148}, year = {2013}, month = {November}, publisher = {Springer Verlag}, series = {Lecture Notes in Computer Science}, volume = {8254}, isbn = {978-3-642-41706-1}, doi = {10.1007/978-3-642-41707-8_9}, url = {http://www.cs.ox.ac.uk/tom.melham/pub/Schrammel-2013-CTC.pdf} }

@inproceedings{Horn:2013:FCL, author = {Alex Horn and Michael Tautschnig and Celina Val and Lihao Liang and Tom Melham and Jim Grundy and Daniel Kroening}, title = {Formal Co-Validation of Low-Level Hardware/Software Interfaces}, booktitle = {{FMCAD} 2013: Formal Methods in Computer-Aided Design: {P}ortland, {O}regon, {USA}, 20--23 {O}ctober 2013}, editor = {Barbara Jobstmann and Sandip Ray}, publisher = {IEEE}, year = {2013}, pages = {121--128}, doi = {10.1109/FMCAD.2013.6679400}, isbn = {978-0-9835678-3-7/13}, url = {http://www.cs.ox.ac.uk/tom.melham/pub/Horn-2013-FCL.pdf} }

@inproceedings{OLeary:2013:RST, author = {John O'Leary and Roope Kaivola and Tom Melham}, title = {Relational {STE} and Theorem Proving for Formal Verification of Industrial Circuit Designs}, booktitle = {{FMCAD} 2013: {F}ormal Methods in Computer-Aided Design: {P}ortland, {O}regon, {USA}, 20--23 {O}ctober 2013}, editor = {Barbara Jobstmann and Sandip Ray}, publisher = {IEEE}, year = {2013}, pages = {97--104}, doi = {10.1109/FMCAD.2013.6679397}, url = {http://www.cs.ox.ac.uk/tom.melham/pub/OLeary-2013-RST.pdf} }

@article{Melham:2013:MAC, author = {Tom Melham}, title = {Modelling, abstraction, and computation in systems biology: A view from computer science}, journal = {Progress in Biophysics and Molecular Biology}, volume = {111}, number = {2-3}, month = {April}, year = {2013}, pages = {129--136}, issn = {0079-6107}, doi = {10.1016/j.pbiomolbio.2012.08.015}, note = {Focussed Issue: Conceptual Foundations of Systems Biology} }

@inproceedings{Khasidashvili:2009:AGV, author = {Zurab Khasidashvili and Gavriel Gavrielov and Tom Melham}, title = {Assume-Guarantee Validation for {STE} Properties within an {SVA} Environment}, booktitle = {Proceedings of 9th International Conference: 2009 Formal Methods in Computer-Aided Design: {FMCAD} 2009}, editor = {Armin Biere and Carl Pixley}, publisher = {IEEE}, year = {2009}, pages = {108--115}, isbn = {978-1-4244-4966-8}, doi = {10.1109/FMCAD.2009.5351133}, url = {http://www.cs.ox.ac.uk/tom.melham/pub/Khasidashvili-2009-AGV.pdf} }

@inproceedings{Hanna:2009:SEF, author = {Ziyad Hanna and Tom Melham}, title = {A Symbolic Execution Framework for Algorithm-Level Modelling}, booktitle = {High Level Design Validation and Test Workshop, 2009. HLDVT 2009.}, editor = {Priyank Kalla and Prabhat Mishra}, publisher = {IEEE}, year = {2009}, pages = {94--99}, isbn = {978-1-4244-4823-4}, issn = {1552-6674}, doi = {10.1109/HLDVT.2009.5340168}, url = {http://www.cs.ox.ac.uk/tom.melham/pub/Hanna-2009-SEF.pdf} }

@inproceedings{Boehm:2008:ARA, author = {Peter B{\"o}hm and Tom Melham}, title = {A Refinement Approach to Design and Verification of On-Chip Communication Protocols}, booktitle = {2008 Formal Methods in Computer Aided Design: {P}ortland, {O}regon, {USA}: 17--20 {N}ovember 2008}, editor = {Alessandro Cimatti and Robert B. Jones}, publisher = {IEEE}, year = {2008}, pages = {136--143}, isbn = {978-1-4244-2735-2}, doi = {10.1109/FMCAD.2008.ECP.22}, url = {http://www.cs.ox.ac.uk/tom.melham/pub/Boehm-2008-ARA.pdf} }

@inproceedings{Boehm:2008:DVOa, author = {Peter B{\"o}hm and Tom Melham}, title = {Design and Verification of On-Chip Communication Protocols}, booktitle = {Seventh International Workshop on {D}esigning {C}orrect {C}ircuits: {B}udapest, 29--30 {M}arch 2008: Participants' Proceedings}, editor = {Gordon J. Pace and Satnam Singh}, publisher = {ETAPS 2008}, note = {A Satellite Event of the {ETAPS} 2008 group of conferences}, year = {2008}, month = {March}, pages = {15--29}, url = {http://www.cs.ox.ac.uk/tom.melham/pub/Boehm-2008-DVOa.pdf} }

@inproceedings{Adams:2007:AAS, author = {Sara Adams and Magnus Bj{\"o}rk and Tom Melham and Carl-Johan Seger}, title = {Automatic Abstraction in Symbolic Trajectory Evaluation}, booktitle = {Formal Methods in Computer Aided Design: {FMCAD} 2007: {N}ovember 11--14 2007, {A}ustin, {T}exas, {USA}}, editor = {Jason Baumgartner and Mary Sheeran}, publisher = {IEEE Computer Society}, year = {2007}, pages = {127--135}, isbn = {978-0-7695-3023-9}, doi = {10.1109/FAMCAD.2007.27}, url = {http://www.cs.ox.ac.uk/tom.melham/pub/Adams-2007-AAS.pdf} }

@inproceedings{Hanna:2007:EVC, author = {Ziyad Hanna and Tom Melham}, title = {Early Validation of Computer Microarchitecture with Algorithm Level Models}, booktitle = {Proceedings of ASM'07: The 14th International Abstract State Machines Workshop}, editor = {Andreas Prinz}, isbn = {978-82-7117-627-3}, year = {2007}, note = {Published electronically}, url = {http://www.cs.ox.ac.uk/tom.melham/pub/Hanna-2007-EVC.pdf} }

@inproceedings{Melham:2006:FHR, author = {Tom Melham and John O'Leary}, title = {A Functional {HDL} in Re{FL}ect}, booktitle = {Sixth International Workshop on {D}esigning {C}orrect {C}ircuits: {V}ienna, 25--26 {M}arch 2006: Participants' Proceedings}, editor = {Mary Sheeran and Tom Melham}, publisher = {ETAPS 2006}, note = {A Satellite Event of the {ETAPS} 2006 group of conferences}, year = {2006}, month = {March}, url = {http://www.cs.ox.ac.uk/tom.melham/pub/Melham-2006-FHR.pdf} }

@proceedings{Sheeran:2006:FIW, editor = {Mary Sheeran and Tom Melham}, title = {Sixth International Workshop on {D}esigning {C}orrect {C}ircuits: {V}ienna, 25--26 {M}arch 2006: Participants' Proceedings}, publisher = {ETAPS 2006}, note = {A Satellite Event of the {ETAPS} 2006 group of conferences}, year = {2006}, month = {March}, url = {http://www.cs.ox.ac.uk/tom.melham/pub/Sheeran-2006-FIW.pdf} }

@article{Grundy:2006:RFL, author = {Jim Grundy and Tom Melham and John O'Leary}, title = {A Reflective Functional Language for Hardware Design and Theorem Proving}, journal = {Journal of Functional Programming}, volume = {16}, number = {2}, month = {March}, year = {2006}, pages = {157--196}, issn = {0956-7968}, eissn = {1469-7653}, doi = {10.1017/S0956796805005757}, url = {http://www.cs.ox.ac.uk/tom.melham/pub/Grundy-2006-RFL.pdf} }

@article{Grundy:2006:TBR, author = {Jim Grundy and Tom Melham and Sava Krsti{\'c} and Sean McLaughlin}, title = {Tool Building Requirements for an {API} to First-Order Solvers}, journal = {Electronic Notes in Theoretical Computer Science}, volume = {144}, number = {2}, month = {January}, year = {2006}, pages = {15--26}, issn = {1571-0661}, doi = {10.1016/j.entcs.2005.12.003}, url = {http://www.cs.ox.ac.uk/tom.melham/pub/Grundy-2006-TBR.pdf} }

@article{Seger:2005:IEE, author = {Carl-Johan H. Seger and Robert B. Jones and John W. O'Leary and Tom Melham and Mark D. Aagaard and Clark Barrett and Don Syme}, title = {An Industrially Effective Environment for Formal Hardware Verification}, journal = {IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems}, volume = {24}, number = {9}, month = {September}, year = {2005}, pages = {1381--1405}, issn = {0278-0070}, doi = {10.1109/TCAD.2005.850814}, url = {http://www.cs.ox.ac.uk/tom.melham/pub/Seger-2005-IEE.pdf} }

@proceedings{Hurd:2005:TPH, editor = {Joe Hurd and Tom Melham}, title = {Theorem Proving in Higher Order Logics: 18th International Conference, {TPHOLs} 2005: {O}xford, {UK}, {A}ugust 22--25, 2005: Proceedings}, booktitle = {Theorem Proving in Higher Order Logics: 18th International Conference, {TPHOLs} 2005: {O}xford, {UK}, {A}ugust 22--25, 2005: Proceedings}, publisher = {Springer-Verlag}, year = {2005}, series = {Lecture Notes in Computer Science}, volume = {3603}, isbn = {3-540-28372-2}, issn = {0302-9743}, doi = {10.1007/11541868}, url = {http://www.springerlink.com/openurl.asp?genre=volume&id=doi:10.1007/11541868} }

@inproceedings{Melham:2004:IMC, author = {Tom Melham}, title = {Integrating Model Checking and Theorem Proving in a Reflective Functional Language}, booktitle = {Integrated Formal Methods: 4th International Conference, {IFM} 2004: {C}anterbury, {UK}, {A}pril 4--7, 2004: Proceedings}, editor = {Eerke A. Boiten and John Derrick and Graeme Smith}, publisher = {Springer-Verlag}, year = {2004}, series = {Lecture Notes in Computer Science}, volume = {2999}, pages = {36--39}, isbn = {3-540-21377-5}, issn = {0302-9743}, url = {http://www.cs.ox.ac.uk/tom.melham/pub/Melham-2004-IMC.pdf} }

@proceedings{Melham:2004:FIW, editor = {Tom Melham and Mary Sheeran}, title = {Fifth International Workshop on {D}esigning {C}orrect {C}ircuits: {B}arcelona, 27--28 {M}arch 2004: Participants' Proceedings}, publisher = {ETAPS 2004}, note = {A Satellite Event of the {ETAPS} 2004 group of conferences}, year = {2004}, month = {March}, url = {http://www.cs.ox.ac.uk/tom.melham/pub/Melham-2004-FIW.pdf} }

@inproceedings{Susanto:2003:AAF, author = {Kong Woei Susanto and Tom Melham}, title = {An {AMBA-ARM7} Formal Verification Platform}, booktitle = {Formal Methods and Software Engineering: 5th International Conference on Formal Engineering Methods, {ICFEM} 2003: {S}ingapore, {N}ovember 5--7, 2003: {P}roceedings}, editor = {Jin Song Dong and Jim Woodcock}, series = {Lecture Notes in Computer Science}, volume = {2885}, publisher = {Springer-Verlag}, year = {2003}, pages = {48--67}, isbn = {3-540-20461-X}, issn = {0302-9743}, url = {http://www.cs.ox.ac.uk/tom.melham/pub/Susanto-2003-AAF.pdf} }

@inproceedings{Melham:2003:AEP, author = {Tom Melham}, title = {Abstract: Experience with Practical Formal Verification at an Industrial Scale}, booktitle = {Proceedings of the Tenth Workshop on Automated Reasoning: Bridging the Gap between Theory and Practice: 15th--16th {A}pril 2003: {L}iverpool}, pages = {1--2}, year = {2003}, organization = {Department of Computer Science, University of Liverpool}, editor = {Clare Dixon}, url = {http://www.cs.ox.ac.uk/tom.melham/pub/Melham-2003-AEP.pdf} }

@article{Dennis:2003:PT, author = {Louise A. Dennis and Graham Collins and Michael Norrish and Richard J. Boulton and Konrad Slind and Thomas F. Melham}, title = {The {PROSPER} toolkit}, journal = {International Journal on Software Tools for Technology Transfer}, volume = {4}, number = {2}, year = {2003}, month = {February}, pages = {189--210}, issn = {1433-2787}, doi = {10.1007/s100090200076}, url = {http://www.springerlink.com/openurl.asp?genre=article&id=doi:10.1007/s100090200076} }

@inproceedings{Melham:2002:ASI, author = {Thomas F. Melham and Robert B. Jones}, title = {Abstraction by Symbolic Indexing Transformations}, booktitle = {Formal Methods in Computer-Aided Design: 4th International Conference, {FMCAD} 2002: {P}ortland, {OR}, {USA}, {N}ovember 6--8, 2002: {P}roceedings}, editor = {Mark D. Aagaard and John W. O'Leary}, series = {Lecture Notes in Computer Science}, volume = {2517}, publisher = {Springer-Verlag}, year = {2002}, pages = {1--18}, isbn = {3-540-00116-6}, issn = {0302-9743}, doi = {https://doi.org/10.1007/3-540-36126-X_1}, url = {http://www.cs.ox.ac.uk/tom.melham/pub/Melham-2002-ASI.pdf} }

@inproceedings{Melham:2002:PAI, author = {Thomas F. Melham}, title = {{PROSPER}: An Investigation into Software Architecture for Embedded Proof Engines}, booktitle = {Frontiers of Combining Systems: 4th International Workshop, {FroCoS} 2002: {S}anta {M}argherita {L}igure, {I}taly, {A}pril 8--10, 2002: Proceedings}, editor = {Alessandro Armando}, publisher = {Springer-Verlag}, year = {2002}, series = {Lecture Notes in Artificial Intelligence}, volume = {2309}, pages = {193--206}, issn = {0302-9743}, isbn = {3-540-43381-3}, url = {http://www.cs.ox.ac.uk/tom.melham/pub/Melham-2002-PAI.pdf} }

@proceedings{Sheeran:2002:DCC, editor = {Mary Sheeran and Tom Melham}, title = {Designing Correct Circuits ({DCC}'02)}, booktitle = {Designing Correct Circuits ({DCC}'02)}, publisher = {ETAPS 2002}, note = {Proceedings of the Workshop on {D}esigning {C}orrect {C}ircuits held during 6--7 {A}pril 2002 in {G}renoble, {F}rance}, month = {April}, year = {2002} }

@proceedings{Margaria:2001:CHD, editor = {Tiziana Margaria and Tom Melham}, title = {Correct Hardware Design and Verification Methods: 11th {IFIP} {WG10.5} Advanced Research Working Conference, {CHARME} 2001: {L}ivingston, {S}cotland, {UK}, {S}eptember 4--7 2001: Proceedings}, booktitle = {Correct Hardware Design and Verification Methods: 11th {IFIP} {WG10.5} Advanced Research Working Conference, {CHARME} 2001: {L}ivingston, {S}cotland, {UK}, {S}eptember 4--7 2001: Proceedings}, publisher = {Springer-Verlag}, year = {2001}, series = {Lecture Notes in Computer Science}, volume = {2144}, isbn = {3-540-42541-1}, issn = {0302-9743}, url = {http://www.springerlink.com/openurl.asp?genre=issue&issn=0302-9743&volume=2144} }

@article{Jones:2001:PFV, author = {Robert B. Jones and John W. O'Leary and Carl-Johan H. Seger and Mark D. Aagaard and Thomas F. Melham}, title = {Practical Formal Verification in Microprocessor Design}, journal = {{IEEE} Design {\&} Test of Computers}, volume = {18}, number = {4}, month = {July/August}, year = {2001}, pages = {16--25}, issn = {0740-7475}, doi = {10.1109/54.936245}, url = {http://www.cs.ox.ac.uk/tom.melham/pub/Jones-2001-PFV.pdf} }

@article{Susanto:2001:FAD, author = {Kong Woei Susanto and Tom Melham}, title = {Formally Analyzed Dynamic Synthesis of Hardware}, journal = {The Journal of Supercomputing}, volume = {19}, number = {1}, month = {May}, year = {2001}, pages = {7--22}, issn = {0920-8542}, doi = {10.1023/A:1011132326153}, url = {http://www.cs.ox.ac.uk/tom.melham/pub/Susanto-2001-FAD.ps} }

@inproceedings{Aagaard:2000:MLH, author = {Mark D. Aagaard and Robert B. Jones and Thomas F. Melham and John W. O'Leary and Carl-Johan H. Seger}, title = {A Methodology for Large-Scale Hardware Verification}, booktitle = {Formal Methods in Computer-Aided Design: Third International Conference, {FMCAD} 2000: {A}ustin, {TX}, {USA}, {N}ovember 1--3, 2000: {P}roceedings}, editor = {Warren A. {Hunt, Jr.} and Steven D. Johnson}, series = {Lecture Notes in Computer Science}, volume = {1954}, publisher = {Springer-Verlag}, year = {2000}, pages = {263--282}, isbn = {3-540-41219-0}, issn = {0302-9743}, url = {http://www.cs.ox.ac.uk/tom.melham/pub/Aagaard-2000-MLH.pdf} }

@article{Aitken:2000:AEI, author = {S. Aitken and T. Melham}, title = {An analysis of errors in interactive proof attempts}, journal = {Interacting with Computers}, volume = {12}, number = {6}, month = {June}, year = {2000}, pages = {565--586}, issn = {0953-5438} }

@inproceedings{Dennis:2000:PT, author = {Louise A. Dennis and Graham Collins and Michael Norrish and Richard Boulton and Konrad Slind and Graham Robinson and Mike Gordon and Tom Melham}, title = {The {PROSPER} Toolkit}, booktitle = {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: {B}erlin, {G}ermany, {M}arch 25 -- {A}pril 2, 2000: {P}roceedings}, editor = {Susanne Graf and Michael Schwartzbach}, series = {Lecture Notes in Computer Science}, volume = {1785}, publisher = {Springer-Verlag}, year = {2000}, pages = {78--92}, isbn = {3-540-67282-6}, issn = {0302-9743}, url = {http://www.cs.ox.ac.uk/tom.melham/pub/Dennis-2000-PT.pdf} }

@inproceedings{Aagaard:1999:XTE, author = {Mark D. Aagaard and Thomas F. Melham and John W. O'Leary}, title = {{X}s Are for Trajectory Evaluation, {B}ooleans Are for Theorem Proving}, booktitle = {Correct Hardware Design and Verification Methods: 10th {IFIP} {WG}10.5 Advanced Research Working Conference, {CHARME'99}: {B}ad {H}errenalb, {G}ermany, {S}eptember 27--29, 1999: {P}roceedings}, editor = {Laurence Pierre and Thomas Kropf}, series = {Lecture Notes in Computer Science}, volume = {1703}, publisher = {Springer-Verlag}, year = {1999}, pages = {202--218}, isbn = {3-540-66559-5}, issn = {0302-9743}, url = {http://www.cs.ox.ac.uk/tom.melham/pub/Aagaard-1999-XTE.pdf} }

@article{Melham:1999:SIT, author = {Tom Melham}, title = {Special Issue on Theorem Provers and Functional Programming}, journal = {Journal of Functional Programming}, volume = {9}, number = {2}, month = {March}, year = {1999}, pages = {i-ii} }

@inproceedings{Susanto:1998:FAD, author = {Kong Woei Susanto and Tom Melham}, title = {Formally Analysed Dynamic Synthesis of Hardware}, booktitle = {Theorem Proving in Higher Order Logics: Emerging Trends: 11th International Conference, {TPHOL}s'98, {C}anberra, {S}eptember 27 -- {O}ctober 1, 1998: Supplementary Proceedings}, editor = {Jim Grundy and Malcolm Newey}, publisher = {Australian National University}, year = {1998}, pages = {105--117}, isbn = {0-7315-4800-0} }

@inproceedings{McKay:1998:DSX, author = {Nicholas McKay and Tom Melham and Kong Woei Susanto and Satnam Singh}, title = {Dynamic Specialisation of {XC6200} {FPGA}s by Partial Evaluation}, booktitle = {Proceedings: {IEEE} Symposium on {FPGA}s for Custom Computing Machines: {A}pril 15--17, 1998, {N}apa {V}alley, {C}alifornia}, editor = {Kenneth L. Pocek and Jeffrey M. Arnold}, publisher = {IEEE Computer Society}, year = {1998}, pages = {308--309}, isbn = {0-8186-8900-5}, url = {http://www.cs.ox.ac.uk/tom.melham/pub/McKay-1998-DSX.pdf} }

@article{Aitken:1998:ITP, author = {J. S. Aitken and P. Gray and T. Melham and M. Thomas}, title = {Interactive Theorem Proving: An Empirical Study of User Activity}, journal = {Journal of Symbolic Computation}, volume = {25}, number = {2}, month = {February}, year = {1998}, pages = {263--284}, issn = {0747-7171} }

@inproceedings{Gordon:1996:FAA, author = {Andrew D. Gordon and Tom Melham}, title = {Five Axioms of Alpha-Conversion}, booktitle = {Theorem Proving in Higher Order Logics: 9th International Conference, {TPHOL}s'96: {T}urku, {F}inland, {A}ugust 26--30, 1996: Proceedings}, editor = {J. von Wright and J. Grundy and J. Harrison}, series = {Lecture Notes in Computer Science}, volume = {1125}, publisher = {Springer-Verlag}, year = {1996}, pages = {173--190}, isbn = {3-540-61587-3}, issn = {0302-9743}, url = {http://www.cs.ox.ac.uk/tom.melham/pub/Gordon-1996-FAA.pdf} }

@inproceedings{Aitken:1996:PMI, author = {J. S. Aitken and P. Gray and T. Melham and M. Thomas}, title = {Phases, Modes and Information Flow in Theory Development}, booktitle = {User Interfaces for Theorem Provers: An International Workshop organised at the {D}epartment of {C}omputer {S}cience, {U}niversity of {Y}ork: 19th {J}uly 1996}, editor = {Nicholas A. Merriam}, publisher = {University of York}, year = {1996}, pages = {1--8} }

@inproceedings{Aitken:1995:IPD, author = {Stuart Aitken and Philip Gray and Tom Melham and Muffy Thomas}, title = {Interactive Proof Discovery: An Empirical Study of {HOL} Users}, booktitle = {User Interface Design for Theorem Proving Systems: An International Workshop organised by the {ITP} Project}, editor = {Philip Gray}, publisher = {Department of Computing Science, University of Glasgow}, year = {1995}, url = {http://www.cs.ox.ac.uk/tom.melham/pub/Aitken-1995-IPD.pdf} }

@proceedings{Melham:1994:HOL, editor = {Thomas F. Melham and Juanito Camilleri}, title = {Higher Order Logic Theorem Proving and Its Applications: 7th International Workshop: {V}alletta, {M}alta, {S}eptember 19--22, 1994: Proceedings}, booktitle = {Higher Order Logic Theorem Proving and Its Applications: 7th International Workshop, {V}alletta, {M}alta, {S}eptember 19--22, 1994: Proceedings}, publisher = {Springer-Verlag}, year = {1994}, series = {Lecture Notes in Computer Science}, volume = {859}, isbn = {3-640-58450-1} }

@proceedings{Melham:1994:SPI, editor = {Tom Melham and Juanito Camilleri}, title = {Supplementary Proceedings of the 7th International Workshop on Higher Order Logic Theorem Proving and its Applications}, booktitle = {Supplementary Proceedings of the 7th International Workshop on Higher Order Logic Theorem Proving and its Applications}, publisher = {University of Malta}, month = {September}, year = {1994} }

@article{Melham:1994:MTP, author = {T. F. Melham}, title = {A Mechanized Theory of the {$\Pi$}-calculus in {HOL}}, journal = {Nordic Journal of Computing}, volume = {1}, number = {1}, year = {1994}, pages = {50--76}, issn = {1236-6064} }

@article{Melham:1994:HLE, author = {Thomas F. Melham}, title = {The {HOL} Logic Extended with Quantification over Type Variables}, journal = {Formal Methods in System Design}, volume = {3}, number = {1--2}, year = {1994}, pages = {7--24}, issn = {0925-9856}, url = {http://www.cs.ox.ac.uk/tom.melham/pub/Melham-1994-HLE.pdf} }

@inproceedings{Melham:1993:HLE, author = {Thomas F. Melham}, title = {The {HOL} Logic Extended with Quantification over Type Variables}, booktitle = {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: {L}euven, {B}elgium, 21--24 {S}eptember 1992}, editor = {Luc J. M. Claesen and Michael J. C. Gordon}, series = {IFIP Transactions A}, volume = {20}, publisher = {North-Holland}, year = {1993}, pages = {3--17}, issn = {0926-5473}, isbn = {0-444-89880-8} }

@inproceedings{Jacobs:1993:TDT, author = {Bart Jacobs and Tom Melham}, title = {Translating Dependent Type Theory into Higher Order Logic}, booktitle = {Typed Lambda Calculi and Applications: International Conference on Typed Lamda Calculi and Applications: {TLCA '93}: {M}arch, 16--18, 1993, {U}trecht, {T}he {N}etherlands: Proceedings}, editor = {M. Bezem and J. F. Groote}, series = {Lecture Notes in Computer Science}, volume = {664}, publisher = {Springer-Verlag}, year = {1993}, pages = {209--229}, isbn = {3-540-56517-5} }

@book{Gordon:1993:ITH, editor = {M. J. C. Gordon and T. F. Melham}, title = {Introduction to {HOL}: A theorem proving environment for higher order logic}, publisher = {Cambridge University Press}, year = {1993}, isbn = {0-521-44189-7}, url = {http://www.cs.ox.ac.uk/tom.melham/pub/Gordon-1993-ITH.html} }

@book{Melham:1993:HOL, author = {T. Melham}, title = {Higher Order Logic and Hardware Verification}, publisher = {Cambridge University Press}, year = {1993}, series = {Cambridge Tracts in Theoretical Computer Science}, volume = {31}, isbn = {0-521-41718-X}, doi = {10.1017/CBO9780511569845}, url = {http://www.cs.ox.ac.uk/tom.melham/pub/Melham-1993-HOL.html} }

@inproceedings{Melham:1992:PIR, author = {T. F. Melham}, title = {A Package for Inductive Relation Definitions in {HOL}}, booktitle = {Proceedings of the 1991 International Workshop on the {HOL} Theorem Proving System and its Applications, {D}avis, {C}alifornia, {A}ugust 28--30, 1991}, editor = {Myla Archer and Jeffrey J. Joyce and Karl N. Levitt and Phillip J. Windley}, publisher = {IEEE Computer Society Press}, year = {1992}, pages = {350--357}, isbn = {0-8186-2460-4}, url = {http://www.cs.ox.ac.uk/tom.melham/pub/Melham-1992-PIR.pdf} }

@proceedings{Stavridou:1992:TPC, editor = {V. Stavridou and T. F. Melham and R. T. Boute}, title = {Theorem Provers in Circuit Design: Proceedings of the {IFIP} {TC}10/{WG} 10.2 International Conference on Theorem Provers in Circuit Design: Theory, Practice, and Experience: {N}ijmegen, {T}he {N}etherlands, 22--24 {J}une 1992}, booktitle = {Theorem Provers in Circuit Design: Proceedings of the {IFIP} {TC}10/{WG} 10.2 International Conference on Theorem Provers in Circuit Design: Theory, Practice, and Experience: {N}ijmegen, {T}he {N}etherlands, 22--24 {J}une 1992}, publisher = {North-Holland}, year = {1992}, series = {IFIP Transactions A}, volume = {10}, isbn = {0-444-89686-4}, issn = {0926-5473} }

@inproceedings{Melham:1991:MTP, author = {T. F. Melham}, title = {A Mechanized Theory of the {$\pi$}-calculus in {HOL}}, booktitle = {Proceedings of the Second Workshop on Logical Frameworks}, editor = {G. Huet and G. Plotkin}, publisher = {University of Edinburgh}, year = {1991}, pages = {219--237}, note = {Preliminary proceedings, published electronically after the workshop} }

@incollection{Melham:1990:AMH, author = {Thomas F. Melham}, title = {Abstraction Mechanisms for Hardware Verification}, booktitle = {Formal Verification of Hardware Design}, editor = {Michael Yoeli}, publisher = {IEEE Computer Society Press}, year = {1990}, pages = {30--49}, isbn = {0-8186-9017-8} }

@phdthesis{Melham:1989:FAM, author = {Thomas Frederick Melham}, title = {Formalizing Abstraction Mechanisms for Hardware Verification in Higher Order Logic}, school = {University of Cambridge}, month = {August}, year = {1989} }

@incollection{Melham:1989:ART, author = {Thomas F. Melham}, title = {Automating Recursive Type Definitions in Higher Order Logic}, booktitle = {Current Trends in Hardware Verification and Automated Theorem Proving}, editor = {G. Birtwistle and P. A. Subrahmanyam}, publisher = {Springer-Verlag}, year = {1989}, pages = {341--386}, isbn = {0-387-96988-8}, isbn = {3-540-96988-8}, url = {http://www.cs.ox.ac.uk/tom.melham/pub/Melham-1989-ART.pdf} }

@incollection{Melham:1988:AMH, author = {Thomas F. Melham}, title = {Abstraction Mechanisms for Hardware Verification}, booktitle = {{VLSI} Specification, Verification and Synthesis}, editor = {Graham Birtwistle and P. A. Subrahmanyam}, publisher = {Kluwer Academic Publishers}, year = {1988}, series = {The Kluwer International Series in Engineeering and Computer Science}, volume = {SECS35}, pages = {267--291}, isbn = {0-89838-246-7} }

@inproceedings{Melham:1988:URT, author = {Thomas F. Melham}, title = {Using Recursive Types to Reason about Hardware in Higher Order Logic}, booktitle = {The Fusion of Hardware Design and Verification: Proceedings of the {IFIP} {WG} 10.2 Working Conference on The Fusion of Hardware Design and Verification: {G}lasgow, {S}cotland, 4--6 {J}uly, 1988}, editor = {George J. Milne}, publisher = {North-Holland}, year = {1988}, pages = {27--50}, isbn = {0-444-70532-5} }

@inproceedings{Birtwistle:1988:HVF, author = {G. Birtwistle and B. Graham and T. Melham and R. Schediwy}, title = {Hardware Verification by Formal Proof}, booktitle = {Proceedings of the {C}anadian Conference on Electrical and Computer Engineering, {V}ancouver, {N}ovember 1988}, editor = {V. K. Bhargava}, publisher = {Canadian Society for Electrical Engineering}, year = {1988}, pages = {379--384} }

@inproceedings{Camilleri:1987:HVH, author = {Albert Camilleri and Mike Gordon and Tom Melham}, title = {Hardware Verification using Higher-Order Logic}, booktitle = {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, {G}renoble, {F}rance, 9--11 {S}eptember, 1986}, editor = {Dominique Borrione}, publisher = {North-Holland}, year = {1987}, pages = {43--67}, isbn = {0-444-70194-X} }

@inproceedings{Birtwistle:1986:SVD, author = {Graham Birtwistle and Jeff Joyce and Breen Liblong and Tom Melham and Rick Schediwy}, title = {Specification and {VLSI} Design}, booktitle = {Formal Aspects of {VLSI} Design: Proceedings of the 1985 {E}dinburgh Workshop on {VLSI}: {E}dinburgh, {S}cotland, {U.K.}}, editor = {George J. Milne and P. A. Subrahmanyam}, publisher = {North-Holland}, year = {1986}, pages = {83--97}, isbn = {0-444-70026-9} }

@article{Liblong:1985:TVD, author = {Breen Liblong and Tom Melham and Graham Birtwistle and John Kendall}, title = {Towards a {VLSI} Design Tool System}, journal = {{INFOR}: Information Systems and Operational Research}, volume = {23}, number = {4}, month = {November}, year = {1985}, pages = {389--402}, issn = {0315-5986} }

@inproceedings{Liblong:1984:TVD, author = {Breen Liblong and Tom Melham and Graham Birtwistle and John Kendall}, title = {Towards a {VLSI} Design Tool System}, booktitle = {{C}anadian Information Processing Society: {SESSION} 84: {P}roceedings}, editor = {Leo Gotlieb}, publisher = {Canadian Information Processing Society}, pages = {37--42}, year = {1984}, issn = {0825-5407} }

@inproceedings{Liblong:1984:EHE, author = {B. Liblong and T. Melham and G. Birtwistle}, title = {Exploiting Hierarchies in {EDICT}}, booktitle = {Proceedings of the 1984 {C}anadian Conference on {VLSI}}, year = {1984} }

@comment{{Research and Technical Reports}}

@article{Jeppu:2021:ALAE, author = {Natasha Yogananda Jeppu and Tom Melham and Daniel Kroening}, title = {Active Learning of Abstract System Models from Traces using Model Checking [Extended]}, journal = {arXiv Computing Research Repository}, volume = {arXiv:2112.05990 [cs.FL]}, year = {2021}, month = {December}, url = {https://arxiv.org/abs/2112.05990} }

@inproceedings{Dunn:2021:EPUA, author = {Isaac Dunn and Hadrien Pouget and Daniel Kroening and Tom Melham}, title = {Exposing Previously Undetectable Faults in Deep Neural Networks}, journal = {arXiv Computing Research Repository}, volume = {arXiv:2106.00576 [cs.LG]}, year = {2021}, month = {June}, url = {https://arxiv.org/abs/2106.00576} }

@article{Alshmarany:2021:THA, author = {Kaled Alshmrany and Ahmed Bhayat and Lucas Cordeiro and Konstantin Korovin and Tom Melham and Mustafa A. Mustafa and Pierre Olivier and Giles Reger and Fedor Shmarov}, title = {Towards a Hybrid Approach to Protect Against Memory Safety Vulnerabilities}, journal = {TechRxiv}, note = {Preprint}, year = {2021}, url = {https://doi.org/10.36227/techrxiv.14680185.v2} }

@article{Williams:2020:ADM, author = {Rebecca Williams and Thomas Melham}, title = {Automated decision-making in the public sector}, year = {2020}, month = {December}, day = {8}, note = {Resource ID w 028 6934}, url = {http://www.cs.ox.ac.uk/tom.melham/pub/Williams-2020-ADM.pdf}, journal = {Practical Law Public Sector} }

@article{Dunn:2020:IDR, author = {Isaac Dunn and Laura Hanu and Hadrien Pouget and Daniel Kroening and Tom Melham}, title = {Evaluating Robustness to Context-Sensitive Feature Perturbations of Different Granularities}, journal = {arXiv Computing Research Repository}, volume = {arXiv:2001.11055 [cs.CV]}, year = {2020}, month = {June}, url = {https://arxiv.org/abs/2001.11055} }

@article{Jeppu:2020:LCMb, author = {Natasha Yogananda Jeppu and Tom Melham and Daniel Kroening and John O'Leary}, title = {Learning Concise Models from Long Execution Traces}, journal = {arXiv Computing Research Repository}, volume = {arXiv:2001.05230 [cs.FL]}, year = {2020}, month = {January}, url = {https://arxiv.org/abs/2001.05230} }

@article{Mukherjee:2020:HSC, author = {Rajdeep Mukherjee and Saurahb Joshi and John O'Leary and Daniel Kroening and Tom Melham}, title = {Hardware/Software Co-verification Using Path-based Symbolic Execution}, journal = {arXiv Computing Research Repository}, volume = {arXiv:2001.01324 [cs.FL]}, year = {2020}, month = {January}, url = {https://arxiv.org/abs/2001.01324} }

@article{Hasanbeig:2019:DPS, author = {Mohammadhosein Hasanbeig and Natasha Yogananda Jeppu and Alessandro Abate and Tom Melham and Daniel Kroening}, title = {{DeepSynth}: Program Synthesis for Automatic Task Segmentation in Deep Reinforcement Learning}, journal = {arXiv Computing Research Repository}, volume = {arXiv:1911.10244 [cs.LG]}, year = {2019}, month = {November}, url = {https://arxiv.org/abs/1911.10244} }

@article{Tiemeyer:2019:CHF, author = {Andreas Tiemeyer and Tom Melham and Daniel Kroening and John O'Leary}, title = {{CREST}: Hardware Formal Verification with {ANSI-C} Reference Specifications}, journal = {arXiv Computing Research Repository}, volume = {arXiv:1908.01324 [cs.PL]}, year = {2019}, month = {August}, url = {https://arxiv.org/abs/1908.01324} }

@article{Dunn:2019:GRU, author = {Isaac Dunn and Hadrien Pouget and Tom Melham and Daniel Kroening}, title = {Adaptive Generation of Unrestricted Adversarial Inputs}, journal = {arXiv Computing Research Repository}, volume = {arXiv:1905.02463 [cs.LG]}, year = {2019}, month = {October}, url = {https://arxiv.org/abs/1905.02463} }

@article{Heelan:2018:AHLa, author = {Sean Heelan and Tom Melham and Daniel Kroening}, title = {Automatic Heap Layout Manipulation for Exploitation}, journal = {arXiv Computing Research Repository}, volume = {arXiv:1804.08470 [cs.CR]}, year = {2018}, month = {April}, url = {https://arxiv.org/abs/1804.08470} }

@article{Mukherjee:2017:LCTa, author = {Rajdeep Mukherjee and Peter Schrammel and Leopold Haller and Daniel Kroening and Tom Melham}, title = {Lifting {CDCL} to Template-Based Abstract Domains for Program Verification}, journal = {arXiv Computing Research Repository}, volume = {arXiv:1707.02011 [cs.LO]}, year = {2017}, month = {July}, url = {https://arxiv.org/abs/1707.02011} }

@article{Liang:2016:VTH, author = {Lihao Liang and Paul E. McKenney and Daniel Kroening and Tom Melham}, title = {Verification of the Tree-Based Hierarchical Read-Copy Update in the {Linux} Kernel}, journal = {arXiv Computing Research Repository}, volume = {arXiv:1610:03052 [cs.LO]}, year = {2016}, month = {October} }

@article{Mukherjee:2016:ECFe, author = {Rajdeep Mukherjee and Saurabh Joshi and Andreas Griesmayer and Daniel Kroening and Tom Melham}, title = {Equivalence Checking a Floating-point Unit against a High-level C Model: Extended Version}, journal = {arXiv Computing Research Repository}, volume = {arXiv:1609.00169 [cs.SE]}, year = {2016}, month = {September} }

@techreport{Barrett:2014:PS2, author = {Clark Barrett and Daniel Kroening and Tom Melham}, editor = {Robert Leese and Tom Melham}, title = {Problem Solving for the 21st Century: Efficient Solvers for Satisfiability Modulo Theories}, institution = {London Mathematical Society and the Smith Institute for Industrial Mathematics and System Engineering}, number = {3}, type = {Knowledge Transfer Report}, month = {June}, year = {2014} }

@article{Schrammel:2013:CTCe:, author = {Peter Schrammel and Tom Melham and Daniel Kroening}, title = {Chaining Test Cases for Reactive System Testing (extended version)}, journal = {arXiv Computing Research Repository}, volume = {arXiv:1306.3882 [cs.SE]}, year = {2013}, month = {November}, url = {https://arxiv.org/abs/1306.3882} }

@article{Melham:2013:OSR, author = {Tom Melham and Raphael Cohn and Ian Childs}, title = {On the Semantics of Re{FL}ect as a Basis for a Reflective Theorem Prover}, journal = {arXiv Computing Research Repository}, volume = {arXiv:1309.5742 [cs.LO]}, month = {September}, year = {2013}, url = {https://arxiv.org/abs/1309.5742} }

@techreport{Boehm:2008:DVOb, author = {Peter B{\"o}hm and Tom Melham}, title = {Design and Verification of On-Chip Communication Protocols}, year = {2008}, month = {April}, type = {Research Report}, number = {RR-08-05}, institution = {Oxford University Computing Laboratory}, url = {http://www.cs.ox.ac.uk/tom.melham/pub/Boehm-2008-DVOb.pdf} }

@techreport{Grundy:2003:RFL, author = {Jim Grundy and Tom Melham and John O'Leary}, title = {A Reflective Functional Language for Hardware Design and Theorem Proving}, number = {PRG-RR-03-16}, type = {Research Report}, institution = {Programming Research Group, Oxford University Computing Laboratory}, month = {October}, year = {2003}, url = {http://www.cs.ox.ac.uk/tom.melham/pub/Grundy-2003-RFL.pdf} }

@techreport{Aagaard:2000:XTE, author = {Mark D. Aagaard and Thomas F. Melham and John W. O'Leary}, title = {{X}s are for Trajectory Evaluation, {B}ooleans are for Theorem Proving (Extended Version)}, type = {Technical Report}, number = {TR-2000-52}, institution = {Department of Computing Science, University of Glasgow}, month = {January}, year = {2000}, url = {http://www.cs.ox.ac.uk/tom.melham/pub/Aagaard-2000-XTE.pdf} }

@techreport{Aitken:1997:IPA, author = {Stuart Aitken and Philip Gray and Tom Melham and Muffy Thomas}, title = {{ITP} Project Anthology}, type = {Technical Report}, number = {TR-1997-36}, institution = {Department of Computing Science, University of Glasgow}, month = {November}, year = {1997} }

@techreport{Melham:1996:SRI, author = {Tom F. Melham}, title = {Some Research Issues in Higher Order Logic Theorem Proving}, type = {BRICS Notes Series}, number = {NS-96-7}, institution = {Department of Computer Science, University of Aarhus}, month = {October}, year = {1996}, issn = {0909-3206} }

@incollection{Aitken:1995:SUA, author = {Stuart Aitken and Philip Gray and Tom Melham and Muffy Thomas}, title = {A Study Of User Activity In Interactive Theorem Proving}, booktitle = {Task Centred Approaches To Interface Design: Glasgow Interactive Systems Group Research Review}, editor = {Chris Johnson}, publisher = {Department of Computing Science, University of Glasgow}, note = {GIST Technical Report G95.2}, month = {August}, year = {1995}, pages = {195--218} }

@techreport{Camilleri:1992:RID, author = {Juanito Camilleri and Tom Melham}, title = {Reasoning with Inductively Defined Relations in the {HOL} Theorem Prover}, type = {Technical Report}, number = {265}, institution = {Computer Laboratory, University of Cambridge}, month = {August}, year = {1992}, url = {http://www.cs.ox.ac.uk/tom.melham/pub/Camilleri-1992-RID.pdf} }

@techreport{Melham:1992:MTP, author = {T. F. Melham}, title = {A Mechanized Theory of the {$\pi$}-calculus in {HOL}}, type = {Technical Report}, number = {244}, institution = {Computer Laboratory, University of Cambridge}, month = {January}, year = {1992} }

@manual{Melham:1992:HFL, author = {T. F. Melham}, title = {The {HOL} finite\_sets Library}, organization = {Computer Laboratory, University of Cambridge}, month = {February}, year = {1992} }

@manual{Melham:1992:HPL, author = {T. F. Melham}, title = {The {HOL} pred\_sets Library}, organization = {Computer Laboratory, University of Cambridge}, month = {February}, year = {1992} }

@manual{Melham:1991:HSL, author = {T. F. Melham}, title = {The {HOL} sets Library}, organization = {Computer Laboratory, University of Cambridge}, month = {October}, year = {1991} }

@manual{Melham:1991:HST, author = {T. F. Melham}, title = {The {HOL} string Library}, organization = {Computer Laboratory, University of Cambridge}, month = {June}, year = {1991} }

@techreport{Birtwistle:1988:HVFP, author = {Graham Birtwistle and Brian Graham and Tom Melham and Rick Schediwy }, title = {Hardware Verification by Formal Proof}, type = {Research Report}, number = {88/328/40}, institution = {Department of Computer Science, University of Calgary}, month = {October}, year = {1988} }

@techreport{Melham:1988:ART, author = {Thomas F. Melham}, title = {Automating Recursive Type Definitions in Higher Order Logic}, type = {Technical Report}, number = {146}, institution = {Computer Laboratory, University of Cambridge}, month = {September}, year = {1988} }

@techreport{Melham:1988:RTR, author = {Thomas F. Melham}, title = {Using Recursive Types to Reason about Hardware in Higher Order Logic}, type = {Technical Report}, number = {135}, institution = {Computer Laboratory, University of Cambridge}, month = {May}, year = {1988} }

@techreport{Melham:1987:AMH, author = {Thomas F. Melham}, title = {Abstraction Mechanisms for Hardware Verification}, type = {Technical Report}, number = {106}, institution = {Computer Laboratory, University of Cambridge}, month = {May}, year = {1987} }

@techreport{Camilleri:1986:HVH, author = {Albert Camilleri and Mike Gordon and Tom Melham}, title = {Hardware Verification using Higher-Order Logic}, type = {Technical Report}, number = {91}, institution = {Computer Laboratory, University of Cambridge}, month = {June}, year = {1986} }

@techreport{Birtwistle:1985:SVD, author = {Graham Birtwistle and Jeff Joyce and Breen Liblong and Tom Melham and Rick Schediwy}, title = {Specification and {VLSI} Design}, type = {Research Report}, number = {85/220/33}, institution = {Department of Computer Science, University of Calgary}, month = {November}, year = {1985} }

@techreport{Liblong:1984:TAV, author = {Breen Liblong and Tom Melham and Graham Birtwistle and John Kendall}, title = {Towards a {VLSI} Design Tool System}, type = {Research Report}, number = {84/175/33}, institution = {Department of Computer Science, University of Calgary}, month = {November}, year = {1984} }

@techreport{Birtwistle:1984:EED, author = {Graham Birtwistle and David Hill and John Kendall and Bill Coates and Richard Esau and Wallace Kroeker and Breen Liblong and Erwin Liu and Tom Melham and Rick Schediwy}, title = {{EDICT}: An Environment for Design Using Integrated Circuit Tools}, type = {Research Report}, number = {84/155/13}, institution = {Department of Computer Science, University of Calgary}, month = {June}, year = {1984} }

@comment{{Patents}}

@misc{Melham:ASI:2004, author = {Thomas F. Melham and Robert B. Jones}, title = {Automatic Symbolic Indexing Methods for Formal Verification on a Symbolic Lattice Domain}, year = {2004}, month = {June}, day = {3}, note = {US Patent 7,310,790} }

*This file was generated by
bibtex2html 1.96.*