Skip to main content

Tom Melham : Publications

Click here to download all publications in a single bibtex file

@inproceedings{Jeppu:2022:ALA,
  title = "Active Learning of Abstract System Models from Traces using Model Checking",
  author = "Natasha Yogananda Jeppu and Tom Melham and Daniel Kroening",
  year = "2022",
  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",
  month = "March",
  pages = "100--103",
  publisher = "{IEEE}",
  url = "http://www.cs.ox.ac.uk/tom.melham/pub/Jeppu-2022-ALA.pdf",
  doi = "10.23919/DATE54114.2022.9774595",
}
@inproceedings{Dunn:2021:EPU,
  title = "Exposing Previously Undetectable Faults in Deep Neural Networks",
  author = "Isaac Dunn and Hadrien Pouget and Daniel Kroening and Tom Melham",
  year = "2021",
  booktitle = "{ISSTA} 2021: Proceedings of the 30th {ACM} {SIGSOFT} International Symposium on Software Testing and Analysis",
  editor = "Cristian Cadar and Xiangyu Zhang",
  journal = "arXiv Computing Research Repository",
  month = "June",
  pages = "56--66",
  url = "https://arxiv.org/abs/2106.00576",
  volume = "arXiv:2106.00576 [cs.LG]",
  doi = "10.1145/3460319.3464801",
}
@article{Jeppu:2021:ALAE,
  title = "Active Learning of Abstract System Models from Traces using Model Checking [Extended]",
  author = "Natasha Yogananda Jeppu and Tom Melham and Daniel Kroening",
  year = "2021",
  journal = "arXiv Computing Research Repository",
  month = "December",
  url = "https://arxiv.org/abs/2112.05990",
  volume = "arXiv:2112.05990 [cs.FL]",
}
@inproceedings{Gao:2021:EFV,
  title = "End-to-End Formal Verification of a {RISC-V} Processor Extended with Capability Pointers",
  author = "Dapeng Gao and Tom Melham",
  year = "2021",
  booktitle = "Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design –- {FMCAD} 2021",
  editor = "Ruzica Piskac and Michael W.~Whalen",
  month = "October",
  pages = "24--33",
  publisher = "TUI Wien Academic Press",
  url = "http://www.cs.ox.ac.uk/tom.melham/pub/Gao-2021-EFVG.pdf",
  volume = "2",
  doi = "10.34727/2021/isbn.978-3-85448-046-4_10",
}
@article{Alshmarany:2021:THA,
  title = "Towards a Hybrid Approach to Protect Against Memory Safety Vulnerabilities",
  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",
  year = "2021",
  journal = "TechRxiv",
  note = "Preprint",
  url = "https://doi.org/10.36227/techrxiv.14680185.v2",
}
@inproceedings{Hasanbeig:2021:DAS,
  title = "{DeepSynth}: Automata Synthesis for Automatic Task Segmentation in Deep Reinforcement Learning",
  author = "Mohammadhosein Hasanbeig and Natasha Yogananda Jeppu and Alessandro Abate and Tom Melham and Daniel Kroening",
  year = "2021",
  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",
  url = "https://ojs.aaai.org/index.php/AAAI/article/view/16935",
}
@article{Dunn:2020:IDR,
  title = "Evaluating Robustness to Context-Sensitive Feature Perturbations of Different Granularities",
  author = "Isaac Dunn and Laura Hanu and Hadrien Pouget and Daniel Kroening and Tom Melham",
  year = "2020",
  journal = "arXiv Computing Research Repository",
  month = "June",
  url = "https://arxiv.org/abs/2001.11055",
  volume = "arXiv:2001.11055 [cs.CV]",
}
@article{Dunn:2020:IDR,
  title = "Investigating Distributional Robustness: Semantic Perturbations Using Generative Models",
  author = "Isaac Dunn and Laura Hanu and Hadrien Pouget and Daniel Kroening and Tom Melham",
  year = "2020",
  journal = "arXiv Computing Research Repository",
  month = "June",
  url = "https://arxiv.org/abs/2001.11055",
  volume = "arXiv:2001.11055 [cs.CV]",
}
@article{Williams:2020:ADM,
  title = "Automated decision-making in the public sector",
  author = "Rebecca Williams and Thomas Melham",
  year = "2020",
  journal = "Practical Law Public Sector",
  month = "December",
  note = "Resource ID w 028 6934",
  url = "http://www.cs.ox.ac.uk/tom.melham/pub/Williams-2020-ADM.pdf",
}
@inproceedings{Vidgen:2020:RCI,
  title = "Recalibrating classifiers for interpretable abusive content detection",
  author = "Bertie Vidgen and Sam Staton and Scott Hale and Ohad Kammar and Helen Margetts and Tom Melham and Marcin Szymczak",
  year = "2020",
  booktitle = "Proceedings of the Fourth Workshop on Natural Language Processing and Computational Social Science",
  month = "November",
  pages = "132--138",
  publisher = "Association for Computational Linguistics",
  url = "https://www.aclweb.org/anthology/2020.nlpcss-1.14",
  doi = "10.18653/v1/2020.nlpcss-1.14",
}
@article{Mukherjee:2020:HSC,
  title = "Hardware/Software Co-verification Using Path-based Symbolic Execution",
  author = "Rajdeep Mukherjee and Saurahb Joshi and John O'Leary and Daniel Kroening and Tom Melham",
  year = "2020",
  journal = "arXiv Computing Research Repository",
  month = "January",
  url = "https://arxiv.org/abs/2001.01324",
  volume = "arXiv:2001.01324 [cs.FL]",
}
@article{Jeppu:2020:LCMb,
  title = "Learning Concise Models from Long Execution Traces",
  author = "Natasha Yogananda Jeppu and Tom Melham and Daniel Kroening and John O'Leary",
  year = "2020",
  journal = "arXiv Computing Research Repository",
  month = "January",
  url = "https://arxiv.org/abs/2001.05230",
  volume = "arXiv:2001.05230 [cs.FL]",
}
@inproceedings{Jeppu:2020:LCMa,
  title = "Learning Concise Models from Long Execution Traces",
  author = "Natasha Yogananda Jeppu and Thomas Melham and Daniel Kroening and John O'Leary",
  year = "2020",
  booktitle = "57th {ACM/IEEE} Design Automation Conference, {DAC} 2020, San Francisco, {CA}, {USA}, July 20--24, 2020",
  pages = "1--6",
  publisher = "IEEE Press",
  doi = "10.1109/DAC18072.2020.9218613",
}
@article{Tiemeyer:2019:CHF,
  title = "{CREST}: Hardware Formal Verification with {ANSI-C} Reference Specifications",
  author = "Andreas Tiemeyer and Tom Melham and Daniel Kroening and John O'Leary",
  year = "2019",
  journal = "arXiv Computing Research Repository",
  month = "August",
  url = "https://arxiv.org/abs/1908.01324",
  volume = "arXiv:1908.01324 [cs.PL]",
}
@article{Hasanbeig:2019:DPS,
  title = "{DeepSynth}: Program Synthesis for Automatic Task Segmentation in Deep Reinforcement Learning",
  author = "Mohammadhosein Hasanbeig and Natasha Yogananda Jeppu and Alessandro Abate and Tom Melham and Daniel Kroening",
  year = "2019",
  journal = "arXiv Computing Research Repository",
  month = "November",
  url = "https://arxiv.org/abs/1911.10244",
  volume = "arXiv:1911.10244 [cs.LG]",
}
@article{Dunn:2019:GRU,
  title = "Adaptive Generation of Unrestricted Adversarial Inputs",
  author = "Isaac Dunn and Hadrien Pouget and Tom Melham and Daniel Kroening",
  year = "2019",
  journal = "arXiv Computing Research Repository",
  month = "October",
  url = "https://arxiv.org/abs/1905.02463",
  volume = "arXiv:1905.02463 [cs.LG]",
}
@inproceedings{Heelan:2019:GMG,
  title = "Gollum: Modular and Greybox Exploit Generation for Heap Overflows in Interpreters",
  author = "Sean Heelan and Tom Melham and Daniel Kroening",
  year = "2019",
  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",
  pages = "1689--1706",
  publisher = "ACM",
  url = "http://www.cs.ox.ac.uk/tom.melham/pub/Heelan-2019-GMG.pdf",
  doi = "10.1145/3319535.3354224",
}
@article{Heelan:2018:AHLa,
  title = "Automatic Heap Layout Manipulation for Exploitation",
  author = "Sean Heelan and Tom Melham and Daniel Kroening",
  year = "2018",
  journal = "arXiv Computing Research Repository",
  month = "April",
  url = "https://arxiv.org/abs/1804.08470",
  volume = "arXiv:1804.08470 [cs.CR]",
}
@inproceedings{Liang:2018:VTB,
  title = "Verification of Tree-Based Hierarchical {Read-Copy Update} in the {Linux} Kernel",
  author = "Lihao Liang and Paul E. McKenney and Daniel Kroening and Tom Melham",
  year = "2018",
  booktitle = "2018 Design, Automation {\&} Test in Europe Conference {\&} Exhibition, {DATE} 2018, Dresden, Germany, March 19--23, 2018",
  editor = "Jan Madsen and Ayse K. Coskun",
  isbn = "978-3-9819263-1-6",
  issn = "1558-1101",
  pages = "61--66",
  publisher = "European Design and Automation Association",
  url = "http://www.cs.ox.ac.uk/tom.melham/pub/Liang-2018-VTB.pdf",
  doi = "10.23919/DATE.2018.8341980",
}
@inproceedings{Heelan:2018:AHL,
  title = "Automatic Heap Layout Manipulation for Exploitation",
  author = "Sean Heelan and Tom Melham and Daniel Kroening",
  year = "2018",
  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",
  pages = "763--779",
  publisher = "{USENIX} Association",
  url = "http://www.cs.ox.ac.uk/tom.melham/pub/Heelan-2018-AHL.pdf",
}
@incollection{Melham:2018:STE,
  title = "Symbolic Trajectory Evaluation",
  author = "Tom Melham",
  year = "2018",
  booktitle = "Handbook of Model Checking",
  chapter = "25",
  editor = "Edmund M. Clarke and Thomas A. Henzinger and Helmut Veith and Roderick Bloem",
  isbn = "978-3-319-10574-1",
  pages = "831--870",
  publisher = "Springer International Publishing",
  doi = "10.1007/978-3-319-10575-8_25",
}
@article{Mukherjee:2017:LCTa,
  title = "Lifting {CDCL} to Template-Based Abstract Domains for Program Verification",
  author = "Rajdeep Mukherjee and Peter Schrammel and Leopold Haller and Daniel Kroening and Tom Melham",
  year = "2017",
  journal = "arXiv Computing Research Repository",
  month = "July",
  url = "https://arxiv.org/abs/1707.02011",
  volume = "arXiv:1707.02011 [cs.LO]",
}
@article{Liang:2017:EVL,
  title = "Effective Verification for Low-Level Software with Competing Interrupts",
  author = "Lihao Liang and Tom Melham and Daniel Kroening and Peter Schrammel and Michael Tautschnig",
  year = "2017",
  issn = "1539-9087",
  journal = "ACM Transactions on Embedded Computing Systems",
  month = "December",
  number = "2",
  pages = "36:1--36:26",
  publisher = "ACM",
  url = "http://www.cs.ox.ac.uk/tom.melham/pub/Liang-2017-EVL.pdf",
  volume = "17",
  doi = "10.1145/3147432",
}
@inproceedings{Mukherjee:2017:LCT,
  title = "Lifting {CDCL} to Template-Based Abstract Domains for Program Verification",
  author = "Rajdeep Mukherjee and Peter Schrammel and Leopold Haller and Daniel Kroening and Tom Melham",
  year = "2017",
  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",
  isbn = "978-3-319-68166-5",
  issn = "0302-9743",
  pages = "307--326",
  publisher = "Springer, Cham",
  series = "Lecture Notes in Computer Science",
  url = "http://www.cs.ox.ac.uk/tom.melham/pub/Mukherjee-2017-LCT.pdf",
  volume = "10482",
  doi = "10.1007/978-3-319-68167-2_21",
}
@article{Mukherjee:2016:ECFe,
  title = "Equivalence Checking a Floating-point Unit against a High-level C Model: Extended Version",
  author = "Rajdeep Mukherjee and Saurabh Joshi and Andreas Griesmayer and Daniel Kroening and Tom Melham",
  year = "2016",
  journal = "arXiv Computing Research Repository",
  month = "September",
  volume = "arXiv:1609.00169 [cs.SE]",
}
@article{Schrammel:GTC:2016,
  title = "Generating test case chains for reactive systems",
  author = "Peter Schrammel and Tom Melham and Daniel Kroening",
  year = "2016",
  issn = "1433-2779",
  journal = "International Journal on Software Tools for Technology Transfer",
  month = "June",
  number = "3",
  pages = "319--334",
  url = "http://www.cs.ox.ac.uk/tom.melham/pub/Schrammel-2016-GTC.pdf",
  volume = "18",
  doi = "10.1007/s10009-014-0358-6",
}
@article{Liang:2016:VTH,
  title = "Verification of the Tree-Based Hierarchical Read-Copy Update in the {Linux} Kernel",
  author = "Lihao Liang and Paul E. McKenney and Daniel Kroening and Tom Melham",
  year = "2016",
  journal = "arXiv Computing Research Repository",
  month = "October",
  volume = "arXiv:1610:03052 [cs.LO]",
}
@inproceedings{Mukherjee:2016:ECF,
  title = "Equivalence Checking of a Floating-Point Unit Against a High-Level {C} Model",
  author = "Rajdeep Mukherjee and Saurabh Joshi and Andreas Griesmayer and Daniel Kroening and Tom Melham",
  year = "2016",
  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",
  isbn = "978-3-319-48988-9",
  issn = "0302-9743",
  pages = "551--558",
  publisher = "Springer-Verlag",
  series = "Lecture Notes in Computer Science",
  volume = "9995",
  doi = "10.1007/978-3-319-48989-6_33",
}
@inproceedings{Mukherjee:2016:USV,
  title = "Unbounded safety verification for hardware using software analyzers",
  author = "Rajdeep Mukherjee and Peter Schrammel and Daniel Kroening and Tom Melham",
  year = "2016",
  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",
  isbn = "978-3-9815370-6-2",
  issn = "1558-1101",
  pages = "1152--1155",
  publisher = "European Design and Automation Association",
  url = "http://www.cs.ox.ac.uk/tom.melham/pub/Mukherjee-2016-USV.pdf",
  doi = "10.3850/9783981537079_0274",
}
@inproceedings{Kroening:2015:EVL,
  title = "Effective Verification of Low-Level Software with Nested Interrupts",
  author = "Daniel Kroening and Lihao Liang and Tom Melham and Peter Schrammel and Michael Tautschnig",
  year = "2015",
  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",
  isbn = "978-3-9815370-4-8",
  pages = "229--234",
  publisher = "{EDA Consortium}",
  url = "http://www.cs.ox.ac.uk/tom.melham/pub/Kroening-2015-EVL.pdf",
}
@inproceedings{Mukherjee:2015:ECU,
  title = "Equivalence Checking Using Trace Partitioning",
  author = "Rajdeep Mukherjee and Daniel Kroening and Tom Melham and Mandayam K. Srivas",
  year = "2015",
  booktitle = "2015 {IEEE} Computer Society Annual Symposium on VLSI, {ISVLSI} 2015, Montpellier, France, July 8-10, 2015",
  pages = "13--18",
  publisher = "{IEEE} Computer Society",
  doi = "10.1109/ISVLSI.2015.110",
}
@inproceedings{Mukherjee:2015:HVU,
  title = "Hardware Verification Using Software Analyzers",
  author = "Rajdeep Mukherjee and Daniel Kroening and Tom Melham",
  year = "2015",
  booktitle = "2015 {IEEE} Computer Society Annual Symposium on VLSI, {ISVLSI} 2015, Montpellier, France, July 8-10, 2015",
  pages = "7--12",
  publisher = "{IEEE} Computer Society",
  doi = "10.1109/ISVLSI.2015.107",
}
@techreport{Barrett:2014:PS2,
  title = "Problem Solving for the 21st Century: Efficient Solvers for Satisfiability Modulo Theories",
  author = "Clark Barrett and Daniel Kroening and Tom Melham",
  year = "2014",
  editor = "Robert Leese and Tom Melham",
  institution = "London Mathematical Society and the Smith Institute for Industrial Mathematics and System Engineering",
  month = "June",
  number = "3",
}
@article{Melham:2013:OSR,
  title = "On the Semantics of Re{FL}ect as a Basis for a Reflective Theorem Prover",
  author = "Tom Melham and Raphael Cohn and Ian Childs",
  year = "2013",
  journal = "arXiv Computing Research Repository",
  month = "September",
  url = "https://arxiv.org/abs/1309.5742",
  volume = "arXiv:1309.5742 [cs.LO]",
}
@article{Melham:2013:MAC,
  title = "Modelling, abstraction, and computation in systems biology: A view from computer science",
  author = "Tom Melham",
  year = "2013",
  issn = "0079-6107",
  journal = "Progress in Biophysics and Molecular Biology",
  month = "April",
  note = "Focussed Issue: Conceptual Foundations of Systems Biology",
  number = "2-3",
  pages = "129--136",
  volume = "111",
  doi = "10.1016/j.pbiomolbio.2012.08.015",
}
@article{Schrammel:2013:CTCe:,
  title = "Chaining Test Cases for Reactive System Testing (extended version)",
  author = "Peter Schrammel and Tom Melham and Daniel Kroening",
  year = "2013",
  journal = "arXiv Computing Research Repository",
  month = "November",
  url = "https://arxiv.org/abs/1306.3882",
  volume = "arXiv:1306.3882 [cs.SE]",
}
@inproceedings{Schrammel:CTC:2013,
  title = "Chaining Test Cases for Reactive System Testing",
  author = "Peter Schrammel and Tom Melham and Daniel Kroening",
  year = "2013",
  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",
  isbn = "978-3-642-41706-1",
  month = "November",
  pages = "133--148",
  publisher = "Springer Verlag",
  series = "Lecture Notes in Computer Science",
  url = "http://www.cs.ox.ac.uk/tom.melham/pub/Schrammel-2013-CTC.pdf",
  volume = "8254",
  doi = "10.1007/978-3-642-41707-8_9",
}
@inproceedings{Horn:2013:FCL,
  title = "Formal Co-Validation of Low-Level Hardware/Software Interfaces",
  author = "Alex Horn and Michael Tautschnig and Celina Val and Lihao Liang and Tom Melham and Jim Grundy and Daniel Kroening",
  year = "2013",
  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",
  isbn = "978-0-9835678-3-7/13",
  pages = "121--128",
  publisher = "IEEE",
  url = "http://www.cs.ox.ac.uk/tom.melham/pub/Horn-2013-FCL.pdf",
  doi = "10.1109/FMCAD.2013.6679400",
}
@inproceedings{OLeary:2013:RST,
  title = "Relational {STE} and Theorem Proving for Formal Verification of Industrial Circuit Designs",
  author = "John O'Leary and Roope Kaivola and Tom Melham",
  year = "2013",
  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",
  isbn = "978-0-9835678-3-7/13",
  pages = "97--104",
  publisher = "IEEE",
  url = "http://www.cs.ox.ac.uk/tom.melham/pub/OLeary-2013-RST.pdf",
  doi = "10.1109/FMCAD.2013.6679397",
}
@inproceedings{Hanna:2009:SEF,
  title = "A Symbolic Execution Framework for Algorithm-Level Modelling",
  author = "Ziyad Hanna and Tom Melham",
  year = "2009",
  booktitle = "High Level Design Validation and Test Workshop, 2009. HLDVT 2009.",
  editor = "Priyank Kalla and Prabhat Mishra",
  isbn = "978-1-4244-4823-4",
  issn = "1552-6674",
  pages = "94--99",
  publisher = "IEEE",
  url = "http://www.cs.ox.ac.uk/tom.melham/pub/Hanna-2009-SEF.pdf",
  doi = "10.1109/HLDVT.2009.5340168",
}
@inproceedings{Khasidashvili:2009:AGV,
  title = "Assume-Guarantee Validation for {STE} Properties within an {SVA} Environment",
  author = "Zurab Khasidashvili and Gavriel Gavrielov and Tom Melham",
  year = "2009",
  booktitle = "Proceedings of 9th International Conference: 2009 Formal Methods in Computer-Aided Design: {FMCAD} 2009",
  editor = "Armin Biere and Carl Pixley",
  isbn = "978-1-4244-4966-8",
  pages = "108--115",
  publisher = "IEEE",
  url = "http://www.cs.ox.ac.uk/tom.melham/pub/Khasidashvili-2009-AGV.pdf",
  doi = "10.1109/FMCAD.2009.5351133",
}
@techreport{Boehm:2008:DVOb,
  title = "Design and Verification of On-Chip Communication Protocols",
  author = "Peter B{\"o}hm and Tom Melham",
  year = "2008",
  institution = "Oxford University Computing Laboratory",
  month = "April",
  number = "RR-08-05",
  url = "http://www.cs.ox.ac.uk/tom.melham/pub/Boehm-2008-DVOb.pdf",
}
@inproceedings{Boehm:2008:DVOa,
  title = "Design and Verification of On-Chip Communication Protocols",
  author = "Peter B{\"o}hm and Tom Melham",
  year = "2008",
  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",
  month = "March",
  note = "A Satellite Event of the {ETAPS} 2008 group of conferences",
  pages = "15--29",
  publisher = "ETAPS 2008",
  url = "http://www.cs.ox.ac.uk/tom.melham/pub/Boehm-2008-DVOa.pdf",
}
@inproceedings{Boehm:2008:ARA,
  title = "A Refinement Approach to Design and Verification of On-Chip Communication Protocols",
  author = "Peter B{\"o}hm and Tom Melham",
  year = "2008",
  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",
  isbn = "978-1-4244-2735-2",
  pages = "136--143",
  publisher = "IEEE",
  url = "http://www.cs.ox.ac.uk/tom.melham/pub/Boehm-2008-ARA.pdf",
  doi = "10.1109/FMCAD.2008.ECP.22",
}
@inproceedings{Hanna:2007:EVC,
  title = "Early Validation of Computer Microarchitecture with Algorithm Level Models",
  author = "Ziyad Hanna and Tom Melham",
  year = "2007",
  booktitle = "Proceedings of ASM'07: The 14th International Abstract State Machines Workshop",
  editor = "Andreas Prinz",
  isbn = "978-82-7117-627-3",
  note = "Published electronically",
  url = "http://www.cs.ox.ac.uk/tom.melham/pub/Hanna-2007-EVC.pdf",
}
@inproceedings{Adams:2007:AAS,
  title = "Automatic Abstraction in Symbolic Trajectory Evaluation",
  author = "Sara Adams and Magnus Bj{\"o}rk and Tom Melham and Carl-Johan Seger",
  year = "2007",
  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",
  isbn = "978-0-7695-3023-9",
  pages = "127--135",
  publisher = "IEEE Computer Society",
  url = "http://www.cs.ox.ac.uk/tom.melham/pub/Adams-2007-AAS.pdf",
  doi = "10.1109/FAMCAD.2007.27",
}
@article{Grundy:2006:RFL,
  title = "A Reflective Functional Language for Hardware Design and Theorem Proving",
  author = "Jim Grundy and Tom Melham and John O'Leary",
  year = "2006",
  issn = "0956-7968",
  journal = "Journal of Functional Programming",
  month = "March",
  number = "2",
  pages = "157--196",
  url = "http://www.cs.ox.ac.uk/tom.melham/pub/Grundy-2006-RFL.pdf",
  volume = "16",
  doi = "10.1017/S0956796805005757",
}
@inproceedings{Melham:2006:FHR,
  title = "A Functional {HDL} in Re{FL}ect",
  author = "Tom Melham and John O'Leary",
  year = "2006",
  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",
  month = "March",
  note = "A Satellite Event of the {ETAPS} 2006 group of conferences",
  publisher = "ETAPS 2006",
  url = "http://www.cs.ox.ac.uk/tom.melham/pub/Melham-2006-FHR.pdf",
}
@proceedings{Sheeran:2006:FIW,
  title = "Sixth International Workshop on {D}esigning {C}orrect {C}ircuits: {V}ienna, 25--26 {M}arch 2006: Participants' Proceedings",
  year = "2006",
  editor = "Mary Sheeran and Tom Melham",
  month = "March",
  note = "A Satellite Event of the {ETAPS} 2006 group of conferences",
  publisher = "ETAPS 2006",
  url = "http://www.cs.ox.ac.uk/tom.melham/pub/Sheeran-2006-FIW.pdf",
}
@article{Grundy:2006:TBR,
  title = "Tool Building Requirements for an {API} to First-Order Solvers",
  author = "Jim Grundy and Tom Melham and Sava Krsti{\'c} and Sean McLaughlin",
  year = "2006",
  issn = "1571-0661",
  journal = "Electronic Notes in Theoretical Computer Science",
  month = "January",
  number = "2",
  pages = "15--26",
  url = "http://www.cs.ox.ac.uk/tom.melham/pub/Grundy-2006-TBR.pdf",
  volume = "144",
  doi = "10.1016/j.entcs.2005.12.003",
}
@article{Seger:2005:IEE,
  title = "An Industrially Effective Environment for Formal Hardware Verification",
  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",
  year = "2005",
  issn = "0278-0070",
  journal = "IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems",
  month = "September",
  number = "9",
  pages = "1381--1405",
  url = "http://www.cs.ox.ac.uk/tom.melham/pub/Seger-2005-IEE.pdf",
  volume = "24",
  doi = "10.1109/TCAD.2005.850814",
}
@proceedings{Hurd:2005:TPH,
  title = "Theorem Proving in Higher Order Logics: 18th International Conference, {TPHOLs} 2005: {O}xford, {UK}, {A}ugust 22--25, 2005: Proceedings",
  year = "2005",
  booktitle = "Theorem Proving in Higher Order Logics: 18th International Conference, {TPHOLs} 2005: {O}xford, {UK}, {A}ugust 22--25, 2005: Proceedings",
  editor = "Joe Hurd and Tom Melham",
  isbn = "3-540-28372-2",
  issn = "0302-9743",
  publisher = "Springer-Verlag",
  series = "Lecture Notes in Computer Science",
  url = "http://www.springerlink.com/openurl.asp?genre=volume&id=doi:10.1007/11541868",
  volume = "3603",
  doi = "10.1007/11541868",
}
@misc{Melham:ASI:2004,
  title = "Automatic Symbolic Indexing Methods for Formal Verification on a Symbolic Lattice Domain",
  author = "Thomas F. Melham and Robert B. Jones",
  year = "2004",
  month = "June",
  note = "US Patent 7,310,790",
}
@proceedings{Melham:2004:FIW,
  title = "Fifth International Workshop on {D}esigning {C}orrect {C}ircuits: {B}arcelona, 27--28 {M}arch 2004: Participants' Proceedings",
  year = "2004",
  editor = "Tom Melham and Mary Sheeran",
  month = "March",
  note = "A Satellite Event of the {ETAPS} 2004 group of conferences",
  publisher = "ETAPS 2004",
  url = "http://www.cs.ox.ac.uk/tom.melham/pub/Melham-2004-FIW.pdf",
}
@inproceedings{Melham:2004:IMC,
  title = "Integrating Model Checking and Theorem Proving in a Reflective Functional Language",
  author = "Tom Melham",
  year = "2004",
  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",
  isbn = "3-540-21377-5",
  issn = "0302-9743",
  pages = "36--39",
  publisher = "Springer-Verlag",
  series = "Lecture Notes in Computer Science",
  url = "http://www.cs.ox.ac.uk/tom.melham/pub/Melham-2004-IMC.pdf",
  volume = "2999",
}
@article{Dennis:2003:PT,
  title = "The {PROSPER} toolkit",
  author = "Louise A. Dennis and Graham Collins and Michael Norrish and Richard J. Boulton and Konrad Slind and Thomas F. Melham",
  year = "2003",
  issn = "1433-2787",
  journal = "International Journal on Software Tools for Technology Transfer",
  month = "February",
  number = "2",
  pages = "189--210",
  url = "http://www.springerlink.com/openurl.asp?genre=article&id=doi:10.1007/s100090200076",
  volume = "4",
  doi = "10.1007/s100090200076",
}
@techreport{Grundy:2003:RFL,
  title = "A Reflective Functional Language for Hardware Design and Theorem Proving",
  author = "Jim Grundy and Tom Melham and John O'Leary",
  year = "2003",
  institution = "Programming Research Group, Oxford University Computing Laboratory",
  month = "October",
  number = "PRG-RR-03-16",
  url = "http://www.cs.ox.ac.uk/tom.melham/pub/Grundy-2003-RFL.pdf",
}
@inproceedings{Melham:2003:AEP,
  title = "Abstract: Experience with Practical Formal Verification at an Industrial Scale",
  author = "Tom Melham",
  year = "2003",
  booktitle = "Proceedings of the Tenth Workshop on Automated Reasoning: Bridging the Gap between Theory and Practice: 15th--16th {A}pril 2003: {L}iverpool",
  editor = "Clare Dixon",
  organization = "Department of Computer Science, University of Liverpool",
  pages = "1--2",
  url = "http://www.cs.ox.ac.uk/tom.melham/pub/Melham-2003-AEP.pdf",
}
@inproceedings{Susanto:2003:AAF,
  title = "An {AMBA-ARM7} Formal Verification Platform",
  author = "Kong Woei Susanto and Tom Melham",
  year = "2003",
  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",
  isbn = "3-540-20461-X",
  issn = "0302-9743",
  pages = "48--67",
  publisher = "Springer-Verlag",
  series = "Lecture Notes in Computer Science",
  url = "http://www.cs.ox.ac.uk/tom.melham/pub/Susanto-2003-AAF.pdf",
  volume = "2885",
}
@proceedings{Sheeran:2002:DCC,
  title = "Designing Correct Circuits ({DCC}'02)",
  year = "2002",
  booktitle = "Designing Correct Circuits ({DCC}'02)",
  editor = "Mary Sheeran and Tom Melham",
  month = "April",
  note = "Proceedings of the Workshop on {D}esigning {C}orrect {C}ircuits held during 6--7 {A}pril 2002 in {G}renoble, {F}rance",
  publisher = "ETAPS 2002",
}
@inproceedings{Melham:2002:PAI,
  title = "{PROSPER}: An Investigation into Software Architecture for Embedded Proof Engines",
  author = "Thomas F. Melham",
  year = "2002",
  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",
  isbn = "3-540-43381-3",
  issn = "0302-9743",
  pages = "193--206",
  publisher = "Springer-Verlag",
  series = "Lecture Notes in Artificial Intelligence",
  url = "http://www.cs.ox.ac.uk/tom.melham/pub/Melham-2002-PAI.pdf",
  volume = "2309",
}
@inproceedings{Melham:2002:ASI,
  title = "Abstraction by Symbolic Indexing Transformations",
  author = "Thomas F. Melham and Robert B. Jones",
  year = "2002",
  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",
  isbn = "3-540-00116-6",
  issn = "0302-9743",
  pages = "1--18",
  publisher = "Springer-Verlag",
  series = "Lecture Notes in Computer Science",
  url = "http://www.cs.ox.ac.uk/tom.melham/pub/Melham-2002-ASI.pdf",
  volume = "2517",
  doi = "https://doi.org/10.1007/3-540-36126-X_1",
}
@article{Susanto:2001:FAD,
  title = "Formally Analyzed Dynamic Synthesis of Hardware",
  author = "Kong Woei Susanto and Tom Melham",
  year = "2001",
  issn = "0920-8542",
  journal = "The Journal of Supercomputing",
  month = "May",
  number = "1",
  pages = "7--22",
  url = "http://www.cs.ox.ac.uk/tom.melham/pub/Susanto-2001-FAD.ps",
  volume = "19",
  doi = "10.1023/A:1011132326153",
}
@article{Jones:2001:PFV,
  title = "Practical Formal Verification in Microprocessor Design",
  author = "Robert B. Jones and John W. O'Leary and Carl-Johan H. Seger and Mark D. Aagaard and Thomas F. Melham",
  year = "2001",
  issn = "0740-7475",
  journal = "{IEEE} Design {\&} Test of Computers",
  month = "July/August",
  number = "4",
  pages = "16--25",
  url = "http://www.cs.ox.ac.uk/tom.melham/pub/Jones-2001-PFV.pdf",
  volume = "18",
  doi = "10.1109/54.936245",
}
@proceedings{Margaria:2001:CHD,
  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",
  year = "2001",
  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",
  editor = "Tiziana Margaria and Tom Melham",
  isbn = "3-540-42541-1",
  issn = "0302-9743",
  publisher = "Springer-Verlag",
  series = "Lecture Notes in Computer Science",
  url = "http://www.springerlink.com/openurl.asp?genre=issue&issn=0302-9743&volume=2144",
  volume = "2144",
}
@article{Aitken:2000:AEI,
  title = "An analysis of errors in interactive proof attempts",
  author = "S. Aitken and T. Melham",
  year = "2000",
  issn = "0953-5438",
  journal = "Interacting with Computers",
  month = "June",
  number = "6",
  pages = "565--586",
  volume = "12",
}
@techreport{Aagaard:2000:XTE,
  title = "{X}s are for Trajectory Evaluation, {B}ooleans are for Theorem Proving (Extended Version)",
  author = "Mark D. Aagaard and Thomas F. Melham and John W. O'Leary",
  year = "2000",
  institution = "Department of Computing Science, University of Glasgow",
  month = "January",
  number = "TR-2000-52",
  url = "http://www.cs.ox.ac.uk/tom.melham/pub/Aagaard-2000-XTE.pdf",
}
@inproceedings{Dennis:2000:PT,
  title = "The {PROSPER} Toolkit",
  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",
  year = "2000",
  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",
  isbn = "3-540-67282-6",
  issn = "0302-9743",
  pages = "78--92",
  publisher = "Springer-Verlag",
  series = "Lecture Notes in Computer Science",
  url = "http://www.cs.ox.ac.uk/tom.melham/pub/Dennis-2000-PT.pdf",
  volume = "1785",
}
@inproceedings{Aagaard:2000:MLH,
  title = "A Methodology for Large-Scale Hardware Verification",
  author = "Mark D. Aagaard and Robert B. Jones and Thomas F. Melham and John W. O'Leary and Carl-Johan H. Seger",
  year = "2000",
  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",
  isbn = "3-540-41219-0",
  issn = "0302-9743",
  pages = "263--282",
  publisher = "Springer-Verlag",
  series = "Lecture Notes in Computer Science",
  url = "http://www.cs.ox.ac.uk/tom.melham/pub/Aagaard-2000-MLH.pdf",
  volume = "1954",
}
@article{Melham:1999:SIT,
  title = "Special Issue on Theorem Provers and Functional Programming",
  author = "Tom Melham",
  year = "1999",
  journal = "Journal of Functional Programming",
  month = "March",
  number = "2",
  pages = "i-ii",
  volume = "9",
}
@inproceedings{Aagaard:1999:XTE,
  title = "{X}s Are for Trajectory Evaluation, {B}ooleans Are for Theorem Proving",
  author = "Mark D. Aagaard and Thomas F. Melham and John W. O'Leary",
  year = "1999",
  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",
  isbn = "3-540-66559-5",
  issn = "0302-9743",
  pages = "202--218",
  publisher = "Springer-Verlag",
  series = "Lecture Notes in Computer Science",
  url = "http://www.cs.ox.ac.uk/tom.melham/pub/Aagaard-1999-XTE.pdf",
  volume = "1703",
}
@article{Aitken:1998:ITP,
  title = "Interactive Theorem Proving: An Empirical Study of User Activity",
  author = "J. S. Aitken and P. Gray and T. Melham and M. Thomas",
  year = "1998",
  issn = "0747-7171",
  journal = "Journal of Symbolic Computation",
  month = "February",
  number = "2",
  pages = "263--284",
  volume = "25",
}
@inproceedings{Susanto:1998:FAD,
  title = "Formally Analysed Dynamic Synthesis of Hardware",
  author = "Kong Woei Susanto and Tom Melham",
  year = "1998",
  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",
  isbn = "0-7315-4800-0",
  pages = "105--117",
  publisher = "Australian National University",
}
@inproceedings{McKay:1998:DSX,
  title = "Dynamic Specialisation of {XC6200} {FPGA}s by Partial Evaluation",
  author = "Nicholas McKay and Tom Melham and Kong Woei Susanto and Satnam Singh",
  year = "1998",
  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",
  isbn = "0-8186-8900-5",
  pages = "308--309",
  publisher = "IEEE Computer Society",
  url = "http://www.cs.ox.ac.uk/tom.melham/pub/McKay-1998-DSX.pdf",
}
@techreport{Aitken:1997:IPA,
  title = "{ITP} Project Anthology",
  author = "Stuart Aitken and Philip Gray and Tom Melham and Muffy Thomas",
  year = "1997",
  institution = "Department of Computing Science, University of Glasgow",
  month = "November",
  number = "TR-1997-36",
}
@techreport{Melham:1996:SRI,
  title = "Some Research Issues in Higher Order Logic Theorem Proving",
  author = "Tom F. Melham",
  year = "1996",
  institution = "Department of Computer Science, University of Aarhus",
  issn = "0909-3206",
  month = "October",
  number = "NS-96-7",
}
@inproceedings{Aitken:1996:PMI,
  title = "Phases, Modes and Information Flow in Theory Development",
  author = "J. S. Aitken and P. Gray and T. Melham and M. Thomas",
  year = "1996",
  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",
  pages = "1--8",
  publisher = "University of York",
}
@inproceedings{Gordon:1996:FAA,
  title = "Five Axioms of Alpha-Conversion",
  author = "Andrew D. Gordon and Tom Melham",
  year = "1996",
  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",
  isbn = "3-540-61587-3",
  issn = "0302-9743",
  pages = "173--190",
  publisher = "Springer-Verlag",
  series = "Lecture Notes in Computer Science",
  url = "http://www.cs.ox.ac.uk/tom.melham/pub/Gordon-1996-FAA.pdf",
  volume = "1125",
}
@incollection{Aitken:1995:SUA,
  title = "A Study Of User Activity In Interactive Theorem Proving",
  author = "Stuart Aitken and Philip Gray and Tom Melham and Muffy Thomas",
  year = "1995",
  booktitle = "Task Centred Approaches To Interface Design: Glasgow Interactive Systems Group Research Review",
  editor = "Chris Johnson",
  month = "August",
  note = "GIST Technical Report G95.2",
  pages = "195--218",
  publisher = "Department of Computing Science, University of Glasgow",
}
@inproceedings{Aitken:1995:IPD,
  title = "Interactive Proof Discovery: An Empirical Study of {HOL} Users",
  author = "Stuart Aitken and Philip Gray and Tom Melham and Muffy Thomas",
  year = "1995",
  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",
  url = "http://www.cs.ox.ac.uk/tom.melham/pub/Aitken-1995-IPD.pdf",
}
@proceedings{Melham:1994:SPI,
  title = "Supplementary Proceedings of the 7th International Workshop on Higher Order Logic Theorem Proving and its Applications",
  year = "1994",
  booktitle = "Supplementary Proceedings of the 7th International Workshop on Higher Order Logic Theorem Proving and its Applications",
  editor = "Tom Melham and Juanito Camilleri",
  month = "September",
  publisher = "University of Malta",
}
@article{Melham:1994:HLE,
  title = "The {HOL} Logic Extended with Quantification over Type Variables",
  author = "Thomas F. Melham",
  year = "1994",
  issn = "0925-9856",
  journal = "Formal Methods in System Design",
  number = "1--2",
  pages = "7--24",
  url = "http://www.cs.ox.ac.uk/tom.melham/pub/Melham-1994-HLE.pdf",
  volume = "3",
}
@article{Melham:1994:MTP,
  title = "A Mechanized Theory of the {$\Pi$}-calculus in {HOL}",
  author = "T. F. Melham",
  year = "1994",
  issn = "1236-6064",
  journal = "Nordic Journal of Computing",
  number = "1",
  pages = "50--76",
  volume = "1",
}
@proceedings{Melham:1994:HOL,
  title = "Higher Order Logic Theorem Proving and Its Applications: 7th International Workshop: {V}alletta, {M}alta, {S}eptember 19--22, 1994: Proceedings",
  year = "1994",
  booktitle = "Higher Order Logic Theorem Proving and Its Applications: 7th International Workshop, {V}alletta, {M}alta, {S}eptember 19--22, 1994: Proceedings",
  editor = "Thomas F. Melham and Juanito Camilleri",
  isbn = "3-640-58450-1",
  publisher = "Springer-Verlag",
  series = "Lecture Notes in Computer Science",
  volume = "859",
}
@book{Gordon:1993:ITH,
  title = "Introduction to {HOL}: A theorem proving environment for higher order logic",
  year = "1993",
  editor = "M. J. C. Gordon and T. F. Melham",
  isbn = "0-521-44189-7",
  publisher = "Cambridge University Press",
  url = "http://www.cs.ox.ac.uk/tom.melham/pub/Gordon-1993-ITH.html",
}
@book{Melham:1993:HOL,
  title = "Higher Order Logic and Hardware Verification",
  author = "T. Melham",
  year = "1993",
  isbn = "0-521-41718-X",
  publisher = "Cambridge University Press",
  series = "Cambridge Tracts in Theoretical Computer Science",
  url = "http://www.cs.ox.ac.uk/tom.melham/pub/Melham-1993-HOL.html",
  volume = "31",
  doi = "10.1017/CBO9780511569845",
}
@inproceedings{Jacobs:1993:TDT,
  title = "Translating Dependent Type Theory into Higher Order Logic",
  author = "Bart Jacobs and Tom Melham",
  year = "1993",
  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",
  isbn = "3-540-56517-5",
  pages = "209--229",
  publisher = "Springer-Verlag",
  series = "Lecture Notes in Computer Science",
  volume = "664",
}
@inproceedings{Melham:1993:HLE,
  title = "The {HOL} Logic Extended with Quantification over Type Variables",
  author = "Thomas F. Melham",
  year = "1993",
  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",
  isbn = "0-444-89880-8",
  issn = "0926-5473",
  pages = "3--17",
  publisher = "North-Holland",
  series = "IFIP Transactions A",
  volume = "20",
}
@techreport{Camilleri:1992:RID,
  title = "Reasoning with Inductively Defined Relations in the {HOL} Theorem Prover",
  author = "Juanito Camilleri and Tom Melham",
  year = "1992",
  institution = "Computer Laboratory, University of Cambridge",
  month = "August",
  number = "265",
  url = "http://www.cs.ox.ac.uk/tom.melham/pub/Camilleri-1992-RID.pdf",
}
@manual{Melham:1992:HPL,
  title = "The {HOL} pred\_sets Library",
  author = "T. F. Melham",
  year = "1992",
  month = "February",
  organization = "Computer Laboratory, University of Cambridge",
}
@manual{Melham:1992:HFL,
  title = "The {HOL} finite\_sets Library",
  author = "T. F. Melham",
  year = "1992",
  month = "February",
  organization = "Computer Laboratory, University of Cambridge",
}
@techreport{Melham:1992:MTP,
  title = "A Mechanized Theory of the {$\pi$}-calculus in {HOL}",
  author = "T. F. Melham",
  year = "1992",
  institution = "Computer Laboratory, University of Cambridge",
  month = "January",
  number = "244",
}
@inproceedings{Melham:1992:PIR,
  title = "A Package for Inductive Relation Definitions in {HOL}",
  author = "T. F. Melham",
  year = "1992",
  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",
  isbn = "0-8186-2460-4",
  pages = "350--357",
  publisher = "IEEE Computer Society Press",
  url = "http://www.cs.ox.ac.uk/tom.melham/pub/Melham-1992-PIR.pdf",
}
@proceedings{Stavridou:1992:TPC,
  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",
  year = "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",
  editor = "V. Stavridou and T. F. Melham and R. T. Boute",
  isbn = "0-444-89686-4",
  issn = "0926-5473",
  publisher = "North-Holland",
  series = "IFIP Transactions A",
  volume = "10",
}
@manual{Melham:1991:HST,
  title = "The {HOL} string Library",
  author = "T. F. Melham",
  year = "1991",
  month = "June",
  organization = "Computer Laboratory, University of Cambridge",
}
@manual{Melham:1991:HSL,
  title = "The {HOL} sets Library",
  author = "T. F. Melham",
  year = "1991",
  month = "October",
  organization = "Computer Laboratory, University of Cambridge",
}
@inproceedings{Melham:1991:MTP,
  title = "A Mechanized Theory of the {$\pi$}-calculus in {HOL}",
  author = "T. F. Melham",
  year = "1991",
  booktitle = "Proceedings of the Second Workshop on Logical Frameworks",
  editor = "G. Huet and G. Plotkin",
  note = "Preliminary proceedings, published electronically after the workshop",
  pages = "219--237",
  publisher = "University of Edinburgh",
}
@incollection{Melham:1990:AMH,
  title = "Abstraction Mechanisms for Hardware Verification",
  author = "Thomas F. Melham",
  year = "1990",
  booktitle = "Formal Verification of Hardware Design",
  editor = "Michael Yoeli",
  isbn = "0-8186-9017-8",
  pages = "30--49",
  publisher = "IEEE Computer Society Press",
}
@phdthesis{Melham:1989:FAM,
  title = "Formalizing Abstraction Mechanisms for Hardware Verification in Higher Order Logic",
  author = "Thomas Frederick Melham",
  year = "1989",
  month = "August",
  school = "University of Cambridge",
}
@incollection{Melham:1989:ART,
  title = "Automating Recursive Type Definitions in Higher Order Logic",
  author = "Thomas F. Melham",
  year = "1989",
  booktitle = "Current Trends in Hardware Verification and Automated Theorem Proving",
  editor = "G. Birtwistle and P. A. Subrahmanyam",
  isbn = "3-540-96988-8",
  pages = "341--386",
  publisher = "Springer-Verlag",
  url = "http://www.cs.ox.ac.uk/tom.melham/pub/Melham-1989-ART.pdf",
}
@techreport{Melham:1988:ART,
  title = "Automating Recursive Type Definitions in Higher Order Logic",
  author = "Thomas F. Melham",
  year = "1988",
  institution = "Computer Laboratory, University of Cambridge",
  month = "September",
  number = "146",
}
@techreport{Melham:1988:RTR,
  title = "Using Recursive Types to Reason about Hardware in Higher Order Logic",
  author = "Thomas F. Melham",
  year = "1988",
  institution = "Computer Laboratory, University of Cambridge",
  month = "May",
  number = "135",
}
@techreport{Birtwistle:1988:HVFP,
  title = "Hardware Verification by Formal Proof",
  author = "Graham Birtwistle and Brian Graham and Tom Melham and Rick Schediwy",
  year = "1988",
  institution = "Department of Computer Science, University of Calgary",
  month = "October",
  number = "88/328/40",
}
@inproceedings{Birtwistle:1988:HVF,
  title = "Hardware Verification by Formal Proof",
  author = "G. Birtwistle and B. Graham and T. Melham and R. Schediwy",
  year = "1988",
  booktitle = "Proceedings of the {C}anadian Conference on Electrical and Computer Engineering, {V}ancouver, {N}ovember 1988",
  editor = "V. K. Bhargava",
  pages = "379--384",
  publisher = "Canadian Society for Electrical Engineering",
}
@inproceedings{Melham:1988:URT,
  title = "Using Recursive Types to Reason about Hardware in Higher Order Logic",
  author = "Thomas F. Melham",
  year = "1988",
  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",
  isbn = "0-444-70532-5",
  pages = "27--50",
  publisher = "North-Holland",
}
@incollection{Melham:1988:AMH,
  title = "Abstraction Mechanisms for Hardware Verification",
  author = "Thomas F. Melham",
  year = "1988",
  booktitle = "{VLSI} Specification, Verification and Synthesis",
  editor = "Graham Birtwistle and P. A. Subrahmanyam",
  isbn = "0-89838-246-7",
  pages = "267--291",
  publisher = "Kluwer Academic Publishers",
  series = "The Kluwer International Series in Engineeering and Computer Science",
  volume = "SECS35",
}
@techreport{Melham:1987:AMH,
  title = "Abstraction Mechanisms for Hardware Verification",
  author = "Thomas F. Melham",
  year = "1987",
  institution = "Computer Laboratory, University of Cambridge",
  month = "May",
  number = "106",
}
@inproceedings{Camilleri:1987:HVH,
  title = "Hardware Verification using Higher-Order Logic",
  author = "Albert Camilleri and Mike Gordon and Tom Melham",
  year = "1987",
  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",
  isbn = "0-444-70194-X",
  pages = "43--67",
  publisher = "North-Holland",
}
@techreport{Camilleri:1986:HVH,
  title = "Hardware Verification using Higher-Order Logic",
  author = "Albert Camilleri and Mike Gordon and Tom Melham",
  year = "1986",
  institution = "Computer Laboratory, University of Cambridge",
  month = "June",
  number = "91",
}
@inproceedings{Birtwistle:1986:SVD,
  title = "Specification and {VLSI} Design",
  author = "Graham Birtwistle and Jeff Joyce and Breen Liblong and Tom Melham and Rick Schediwy",
  year = "1986",
  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",
  isbn = "0-444-70026-9",
  pages = "83--97",
  publisher = "North-Holland",
}
@article{Liblong:1985:TVD,
  title = "Towards a {VLSI} Design Tool System",
  author = "Breen Liblong and Tom Melham and Graham Birtwistle and John Kendall",
  year = "1985",
  issn = "0315-5986",
  journal = "{INFOR}: Information Systems and Operational Research",
  month = "November",
  number = "4",
  pages = "389--402",
  volume = "23",
}
@techreport{Birtwistle:1985:SVD,
  title = "Specification and {VLSI} Design",
  author = "Graham Birtwistle and Jeff Joyce and Breen Liblong and Tom Melham and Rick Schediwy",
  year = "1985",
  institution = "Department of Computer Science, University of Calgary",
  month = "November",
  number = "85/220/33",
}
@techreport{Birtwistle:1984:EED,
  title = "{EDICT}: An Environment for Design Using Integrated Circuit Tools",
  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",
  year = "1984",
  institution = "Department of Computer Science, University of Calgary",
  month = "June",
  number = "84/155/13",
}
@techreport{Liblong:1984:TAV,
  title = "Towards a {VLSI} Design Tool System",
  author = "Breen Liblong and Tom Melham and Graham Birtwistle and John Kendall",
  year = "1984",
  institution = "Department of Computer Science, University of Calgary",
  month = "November",
  number = "84/175/33",
}
@inproceedings{Liblong:1984:EHE,
  title = "Exploiting Hierarchies in {EDICT}",
  author = "B. Liblong and T. Melham and G. Birtwistle",
  year = "1984",
  booktitle = "Proceedings of the 1984 {C}anadian Conference on {VLSI}",
}
@inproceedings{Liblong:1984:TVD,
  title = "Towards a {VLSI} Design Tool System",
  author = "Breen Liblong and Tom Melham and Graham Birtwistle and John Kendall",
  year = "1984",
  booktitle = "{C}anadian Information Processing Society: {SESSION} 84: {P}roceedings",
  editor = "Leo Gotlieb",
  issn = "0825-5407",
  pages = "37--42",
  publisher = "Canadian Information Processing Society",
}