@comment{{Scientific Publications}}
@article{Jeppu:2023:EAM,
  author = {Natasha Yogananda Jeppu and Tom Melham and Daniel Kroening},
  title = {Enhancing active model learning with equivalence checking using simulation relations},
  journal = {Formal Methods in System Design},
  month = {August},
  year = {2023},
  doi = {10.1007/s10703-023-00433-y},
  publisher = {Springer Nature},
  isbn = {1572-8102},
  url = {http://www.cs.ox.ac.uk/tom.melham/pub/Jeppu-2023-EAM.pdf}
}
@inproceedings{Park:2023:FCS,
  author = {Seung Hoon Park and Rekha Pai and Tom Melham},
  title = {A Formal {CHERI-C} Semantics for Verification},
  booktitle = {Tools and Algorithms for the Construction and Analysis of Systems: {TACAS} 2023},
  editor = {Sriram Sankaranarayanan and Natasha Sharygina},
  series = {Lecture Notes in Computer Science},
  volume = {13993},
  pages = {549--568},
  year = {2023},
  publisher = {Springer, Cham},
  url = {http://www.cs.ox.ac.uk/tom.melham/pub/Park-2023-FCS.pdf},
  doi = {10.1007/978-3-031-30823-9_28}
}
@inproceedings{Jeppu:2022:ALA,
  author = {Natasha Yogananda Jeppu and Tom Melham and Daniel Kroening},
  title = {Active Learning of Abstract System Models from Traces using Model Checking},
  booktitle = {2022 Design, Automation {\&} Test in Europe Conference {\&}
               Exhibition, {DATE} 2022, Antwerp, Belgium, March 14-23, 2022},
  editor = {Cristiana Bolchini and Ingrid Verbauwhede and Ioana Vatajelu},
  year = {2022},
  month = {March},
  doi = {10.23919/DATE54114.2022.9774595},
  pages = {100--103},
  publisher = {{IEEE}},
  url = {http://www.cs.ox.ac.uk/tom.melham/pub/Jeppu-2022-ALA.pdf}
}
@inproceedings{Alshmrany:2022:THA,
  author = {Kaled M. Alshmrany and Ahmed Bhayat and Franz Brau{\ss}e and Lucas C. Cordeiro and Konstantin Korovin and
               Tom Melham and Mustafa A. Mustafa and Pierre Olivier and Giles Reger and Fedor Shmarov},
  title = {Position Paper: Towards a Hybrid Approach to Protect Against Memory
               Safety Vulnerabilities},
  booktitle = {{IEEE} Secure Development Conference, SecDev 2022, Atlanta, GA, USA,
                October 18--20, 2022},
  pages = {52--58},
  publisher = {{IEEE}},
  year = {2022},
  doi = {10.1109/SecDev53368.2022.00020}
}
@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},
  url = {https://ojs.aaai.org/index.php/AAAI/article/view/16935},
  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{Park:2023:FCSa,
  author = {Seung Hoon Park and Rekha Pai and Tom Melham},
  title = {A Formal {CHERI-C} Semantics for Verification},
  journal = {arXiv Computing Research Repository},
  volume = {arXiv:2211.07511 [cs.LO]},
  year = {2023},
  month = {January},
  url = {https://arxiv.org/abs/2211.07511}
}
@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}
}
@article{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.

Tom Melham, last updated Sat 12 Aug 2023 07:28:16 BST