A Package for Inductive Relation Definitions in HOL. - Thomas F. Melham (TPHOLs, 1991)

Higher Order Logic and Hardware Verification. - Thomas F. Melham (Cambridge University Press, 1993)

Translating Dependent Type Theory into Higher Order Logic. - Bart Jacobs 001; Thomas F. Melham (TLCA, 1993)

The HOL Logic Extended with Quantification over Type Variables. - Thomas F. Melham (Formal Methods Syst. Des., 1993)

A Mechanized Theory of the Pi-Calculus in HOL. - Thomas F. Melham (Nord. J. Comput., 1994)

Five Axioms of Alpha-Conversion. - Andrew D. Gordon 001; Thomas F. Melham (TPHOLs, 1996)

Dynamic Specialization of XC6200 FPGAs by Partial Evaluation. - Nicholas McKay; Thomas F. Melham; Kong Woei Susanto; Satnam Singh (FCCM, 1998)

Interactive Theorem Proving: An Empirical Study of User Activity. - J. Stuart Aitken; Philip D. Gray; Thomas F. Melham; Muffy Thomas (J. Symb. Comput., 1998)

Xs are for Trajectory Evaluation, Booleans are for Theorem Proving. - Mark D. Aagaard; Thomas F. Melham; John W. O'Leary (CHARME, 1999)

A Methodology for Large-Scale Hardware Verification. - Mark D. Aagaard; Robert B. Jones; Thomas F. Melham; John W. O'Leary; Carl-Johan H. Seger (FMCAD, 2000)

The PROSPER Toolkit. - Louise A. Dennis; Graham Collins; Michael Norrish; Richard J. Boulton; Konrad Slind; Graham Robinson; Michael J. C. Gordon; Thomas F. Melham (TACAS, 2000)

An analysis of errors in interactive proof attempts. - J. Stuart Aitken; Thomas F. Melham (Interact. Comput., 2000)

Practical Formal Verification in Microprocessor Design. - Robert B. Jones; John W. O'Leary; Carl-Johan H. Seger; Mark D. Aagaard; Thomas F. Melham (IEEE Des. Test Comput., 2001)

Formally Analyzed Dynamic Synthesis of Hardware. - Kong Woei Susanto; Thomas F. Melham (J. Supercomput., 2001)

Abstraction by Symbolic Indexing Transformations. - Thomas F. Melham; Robert B. Jones (FMCAD, 2002)

PROSPER - An Investigation into Software Architecture for Embedded Proof Engines. - Thomas F. Melham (FroCoS, 2002)

An AMBA-ARM7 Formal Verification Platform. - Kong Woei Susanto; Thomas F. Melham (ICFEM, 2003)

The PROSPER toolkit. - Louise A. Dennis; Graham Collins; Michael Norrish; Richard J. Boulton; Konrad Slind; Thomas F. Melham (Int. J. Softw. Tools Technol. Transf., 2003)

Integrating Model Checking and Theorem Proving in a Reflective Functional Language. - Thomas F. Melham (IFM, 2004)

Tool Building Requirements for an API to First-Order Solvers. - Jim Grundy; Thomas F. Melham; Sava Krstic; Sean McLaughlin (PDPAR@CAV, 2005)

An industrially effective environment for formal hardware verification. - Carl-Johan H. Seger; Robert B. Jones; John W. O'Leary; Thomas F. Melham; Mark D. Aagaard; Clark W. Barrett; Don Syme (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2005)

A reflective functional language for hardware design and theorem proving. - Jim Grundy; Thomas F. Melham; John W. O'Leary (J. Funct. Program., 2006)

Automatic Abstraction in Symbolic Trajectory Evaluation. - Sara Adams; Magnus Björk; Thomas F. Melham; Carl-Johan H. Seger (FMCAD, 2007)

A Refinement Approach to Design and Verification of On-Chip Communication Protocols. - Peter Böhm; Tom Melham (FMCAD, 2008)

Assume-guarantee validation for STE properties within an SVA environment. - Zurab Khasidashvili; Gavriel Gavrielov; Tom Melham (FMCAD, 2009)

A symbolic execution framework for algorithm-level modelling. - Ziyad Hanna; Thomas F. Melham (HLDVT, 2009)

Formal co-validation of low-level hardware/software interfaces. - Alex Horn; Michael Tautschnig; Celina G. Val; Lihao Liang; Tom Melham; Jim Grundy; Daniel Kroening (FMCAD, 2013)

Relational STE and theorem proving for formal verification of industrial circuit designs. - John W. O'Leary; Roope Kaivola; Tom Melham (FMCAD, 2013)

Chaining Test Cases for Reactive System Testing. - Peter Schrammel; Tom Melham; Daniel Kroening (ICTSS, 2013)

On the Semantics of ReFLect as a Basis for a Reflective Theorem Prover. - Tom Melham; Raphael Cohn; Ian Childs (CoRR, 2013)

Chaining Test Cases for Reactive System Testing (extended version). - Peter Schrammel; Tom Melham; Daniel Kroening (CoRR, 2013)

Effective verification of low-level software with nested interrupts. - Daniel Kroening; Lihao Liang; Tom Melham; Peter Schrammel; Michael Tautschnig (DATE, 2015)

Hardware Verification Using Software Analyzers. - Rajdeep Mukherjee; Daniel Kroening; Tom Melham (ISVLSI, 2015)

Equivalence Checking Using Trace Partitioning. - Rajdeep Mukherjee; Daniel Kroening; Tom Melham; Mandayam K. Srivas (ISVLSI, 2015)

Unbounded safety verification for hardware using software analyzers. - Rajdeep Mukherjee; Peter Schrammel; Daniel Kroening; Tom Melham (DATE, 2016)

Equivalence Checking of a Floating-Point Unit Against a High-Level C Model. - Rajdeep Mukherjee; Saurabh Joshi 001; Andreas Griesmayer; Daniel Kroening; Tom Melham (FM, 2016)

Equivalence Checking a Floating-point Unit against a High-level C Model (Extended Version). - Rajdeep Mukherjee; Saurabh Joshi 001; Andreas Griesmayer; Daniel Kroening; Tom Melham (CoRR, 2016)

Generating test case chains for reactive systems. - Peter Schrammel; Tom Melham; Daniel Kroening (Int. J. Softw. Tools Technol. Transf., 2016)

Lifting CDCL to Template-Based Abstract Domains for Program Verification. - Rajdeep Mukherjee; Peter Schrammel; Leopold Haller; Daniel Kroening; Tom Melham (ATVA, 2017)

Verification of tree-based hierarchical read-copy update in the Linux kernel. - Lihao Liang; Paul E. McKenney; Daniel Kroening; Tom Melham (DATE, 2018)

Automatic Heap Layout Manipulation for Exploitation. - Sean Heelan; Tom Melham; Daniel Kroening (USENIX Security Symposium, 2018)

Effective Verification for Low-Level Software with Competing Interrupts. - Lihao Liang; Tom Melham; Daniel Kroening; Peter Schrammel; Michael Tautschnig (ACM Trans. Embed. Comput. Syst., 2018)

Symbolic Trajectory Evaluation. - Tom Melham (Handbook of Model Checking, 2018)

Gollum: Modular and Greybox Exploit Generation for Heap Overflows in Interpreters. - Sean Heelan; Tom Melham; Daniel Kroening (CCS, 2019)

Generating Realistic Unrestricted Adversarial Inputs using Dual-Objective GAN Training. - Isaac Dunn; Tom Melham; Daniel Kroening (CoRR, 2019)

CREST: Hardware Formal Verification with ANSI-C Reference Specifications. - Andreas Tiemeyer; Tom Melham; Daniel Kroening; John O'Leary (CoRR, 2019)

DeepSynth: Program Synthesis for Automatic Task Segmentation in Deep Reinforcement Learning. - Mohammadhosein Hasanbeig; Natasha Yogananda Jeppu; Alessandro Abate; Tom Melham; Daniel Kroening (CoRR, 2019)

Learning Concise Models from Long Execution Traces. - Natasha Yogananda Jeppu; Thomas F. Melham; Daniel Kroening; John O'Leary (DAC, 2020)

Hardware/Software Co-verification Using Path-based Symbolic Execution. - Rajdeep Mukherjee; Saurabh Joshi 001; John O'Leary; Daniel Kroening; Tom Melham (CoRR, 2020)

Semantic Adversarial Perturbations using Learnt Representations. - Isaac Dunn; Tom Melham; Daniel Kroening (CoRR, 2020)

DeepSynth: Automata Synthesis for Automatic Task Segmentation in Deep Reinforcement Learning. - Mohammadhosein Hasanbeig; Natasha Yogananda Jeppu; Alessandro Abate; Tom Melham; Daniel Kroening (AAAI, 2021)

End-to-End Formal Verification of a RISC-V Processor Extended with Capability Pointers. - Dapeng Gao; Tom Melham (FMCAD, 2021)

Exposing previously undetectable faults in deep neural networks. - Isaac Dunn; Hadrien Pouget; Daniel Kroening; Tom Melham (ISSTA, 2021)

Active Learning of Abstract System Models from Traces using Model Checking [Extended]. - Natasha Yogananda Jeppu; Tom Melham; Daniel Kroening (CoRR, 2021)

Active Learning of Abstract System Models from Traces using Model Checking. - Natasha Yogananda Jeppu; Tom Melham; Daniel Kroening (DATE, 2022)

Position Paper: Towards a Hybrid Approach to Protect Against Memory Safety Vulnerabilities. - Kaled M. Alshmrany; Ahmed Bhayat; Franz Brauße; Lucas C. Cordeiro; Konstantin Korovin; Tom Melham; Mustafa A. Mustafa; Pierre Olivier; Giles Reger; Fedor Shmarov (SecDev, 2022)

Enhancing active model learning with equivalence checking using simulation relations. - Natasha Yogananda Jeppu; Tom Melham; Daniel Kroening (Formal Methods Syst. Des., 2022)

A Formal CHERI-C Semantics for Verification. - Seung Hoon Park; Rekha R. Pai; Tom Melham (TACAS (1), 2023)

Modelling Tool Extension for Vulnerability Management. - Avi Shaked; Nan Messe; Tom Melham (MoDELS (Companion), 2024)

Symbolic Task Inference in Deep Reinforcement Learning. - Hosein Hasanbeig; Natasha Yogananda Jeppu; Alessandro Abate; Tom Melham; Daniel Kroening (J. Artif. Intell. Res., 2024)

Contextualizing Formal Verification for Systems Security Engineering. - Avi Shaked; Tom Melham (IEEE Secur. Priv., 2025)

Comprehensive Formal Verification of Observational Correctness for the CHERIoT-Ibex Processor. - Louis-Emile Ploix; Alasdair Armstrong; Tom Melham; Ray Lin; Haolong Wang; Anastasia Courtney (CoRR, 2025)