Tom Melham

According to our database, Tom Melham authored at least 58 papers between 1991 and 2023.

Collaborative distances:

• Dijkstra number of three.
• Erdős number of four.

2023

A Formal CHERI-C Semantics for Verification.

Seung Hoon Park, Rekha R. Pai, Tom Melham

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2023

2022

Enhancing active model learning with equivalence checking using simulation relations.

Natasha Yogananda Jeppu, Tom Melham, Daniel Kroening

Formal Methods Syst. Des., December, 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

Proceedings of the IEEE Secure Development Conference, 2022

Active Learning of Abstract System Models from Traces using Model Checking.

Natasha Yogananda Jeppu, Tom Melham, Daniel Kroening

Proceedings of the 2022 Design, Automation & Test in Europe Conference & Exhibition, 2022

2021

Active Learning of Abstract System Models from Traces using Model Checking [Extended].

Natasha Yogananda Jeppu, Tom Melham, Daniel Kroening

CoRR, 2021

Exposing previously undetectable faults in deep neural networks.

Isaac Dunn, Hadrien Pouget, Daniel Kroening, Tom Melham

Proceedings of the ISSTA '21: 30th ACM SIGSOFT International Symposium on Software Testing and Analysis, 2021

End-to-End Formal Verification of a RISC-V Processor Extended with Capability Pointers.

Dapeng Gao, Tom Melham

Proceedings of the Formal Methods in Computer Aided Design, 2021

DeepSynth: Automata Synthesis for Automatic Task Segmentation in Deep Reinforcement Learning.

Mohammadhosein Hasanbeig, Natasha Yogananda Jeppu, Alessandro Abate, Tom Melham, Daniel Kroening

Proceedings of the Thirty-Fifth AAAI Conference on Artificial Intelligence, 2021

2020

Semantic Adversarial Perturbations using Learnt Representations.

Isaac Dunn, Tom Melham, Daniel Kroening

CoRR, 2020

Hardware/Software Co-verification Using Path-based Symbolic Execution.

Rajdeep Mukherjee, Saurabh Joshi, John O'Leary, Daniel Kroening, Tom Melham

CoRR, 2020

Learning Concise Models from Long Execution Traces.

Natasha Yogananda Jeppu, Thomas F. Melham, Daniel Kroening, John O'Leary

Proceedings of the 57th ACM/IEEE Design Automation Conference, 2020

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

CREST: Hardware Formal Verification with ANSI-C Reference Specifications.

Andreas Tiemeyer, Tom Melham, Daniel Kroening, John O'Leary

CoRR, 2019

Generating Realistic Unrestricted Adversarial Inputs using Dual-Objective GAN Training.

Isaac Dunn, Tom Melham, Daniel Kroening

CoRR, 2019

Gollum: Modular and Greybox Exploit Generation for Heap Overflows in Interpreters.

Sean Heelan, Tom Melham, Daniel Kroening

Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security, 2019

2018

Symbolic Trajectory Evaluation.

Tom Melham

Proceedings of the Handbook of Model Checking., 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

Automatic Heap Layout Manipulation for Exploitation.

Sean Heelan, Tom Melham, Daniel Kroening

Proceedings of the 27th USENIX Security Symposium, 2018

Verification of tree-based hierarchical read-copy update in the Linux kernel.

Lihao Liang, Paul E. McKenney, Daniel Kroening, Tom Melham

Proceedings of the 2018 Design, Automation & Test in Europe Conference & Exhibition, 2018

2017

Lifting CDCL to Template-Based Abstract Domains for Program Verification.

Rajdeep Mukherjee, Peter Schrammel, Leopold Haller, Daniel Kroening, Tom Melham

Proceedings of the Automated Technology for Verification and Analysis, 2017

2016

Generating test case chains for reactive systems.

Peter Schrammel, Tom Melham, Daniel Kroening

Int. J. Softw. Tools Technol. Transf., 2016

Equivalence Checking a Floating-point Unit against a High-level C Model (Extended Version).

Rajdeep Mukherjee, Saurabh Joshi, Andreas Griesmayer, Daniel Kroening, Tom Melham

CoRR, 2016

Equivalence Checking of a Floating-Point Unit Against a High-Level C Model.

Rajdeep Mukherjee, Saurabh Joshi, Andreas Griesmayer, Daniel Kroening, Tom Melham

Proceedings of the FM 2016: Formal Methods, 2016

Unbounded safety verification for hardware using software analyzers.

Rajdeep Mukherjee, Peter Schrammel, Daniel Kroening, Tom Melham

Proceedings of the 2016 Design, Automation & Test in Europe Conference & Exhibition, 2016

2015

Equivalence Checking Using Trace Partitioning.

Rajdeep Mukherjee, Daniel Kroening, Tom Melham, Mandayam K. Srivas

Proceedings of the 2015 IEEE Computer Society Annual Symposium on VLSI, 2015

Hardware Verification Using Software Analyzers.

Rajdeep Mukherjee, Daniel Kroening, Tom Melham

Proceedings of the 2015 IEEE Computer Society Annual Symposium on VLSI, 2015

Effective verification of low-level software with nested interrupts.

Daniel Kroening, Lihao Liang, Tom Melham, Peter Schrammel, Michael Tautschnig

Proceedings of the 2015 Design, Automation & Test in Europe Conference & Exhibition, 2015

2013

Chaining Test Cases for Reactive System Testing (extended version).

Peter Schrammel, Tom Melham, Daniel Kroening

CoRR, 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.

Peter Schrammel, Tom Melham, Daniel Kroening

Proceedings of the Testing Software and Systems, 2013

Relational STE and theorem proving for formal verification of industrial circuit designs.

John W. O'Leary, Roope Kaivola, Tom Melham

Proceedings of the Formal Methods in Computer-Aided Design, 2013

Formal co-validation of low-level hardware/software interfaces.

Alex Horn, Michael Tautschnig, Celina G. Val, Lihao Liang, Tom Melham, Jim Grundy, Daniel Kroening

Proceedings of the Formal Methods in Computer-Aided Design, 2013

2009

A symbolic execution framework for algorithm-level modelling.

Ziyad Hanna, Thomas F. Melham

Proceedings of the IEEE International High Level Design Validation and Test Workshop, 2009

Assume-guarantee validation for STE properties within an SVA environment.

Zurab Khasidashvili, Gavriel Gavrielov, Tom Melham

Proceedings of 9th International Conference on Formal Methods in Computer-Aided Design, 2009

2008

A Refinement Approach to Design and Verification of On-Chip Communication Protocols.

Peter Böhm, Tom Melham

Proceedings of the Formal Methods in Computer-Aided Design, 2008

2007

Automatic Abstraction in Symbolic Trajectory Evaluation.

Sara Adams, Magnus Björk, Thomas F. Melham, Carl-Johan H. Seger

Proceedings of the Formal Methods in Computer-Aided Design, 7th International Conference, 2007

2006

A reflective functional language for hardware design and theorem proving.

Jim Grundy, Thomas F. Melham, John W. O'Leary

J. Funct. Program., 2006

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

Tool Building Requirements for an API to First-Order Solvers.

Jim Grundy, Thomas F. Melham, Sava Krstic, Sean McLaughlin

Proceedings of the Third Workshop on Pragmatics of Decision Procedures in Automated Reasoning, 2005

2004

Integrating Model Checking and Theorem Proving in a Reflective Functional Language.

Thomas F. Melham

Proceedings of the Integrated Formal Methods, 4th International Conference, 2004

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

An AMBA-ARM7 Formal Verification Platform.

Kong Woei Susanto, Thomas F. Melham

Proceedings of the Formal Methods and Software Engineering, 2003

2002

PROSPER - An Investigation into Software Architecture for Embedded Proof Engines.

Thomas F. Melham

Proceedings of the Frontiers of Combining Systems, 4th International Workshop, 2002

Abstraction by Symbolic Indexing Transformations.

Thomas F. Melham, Robert B. Jones

Proceedings of the Formal Methods in Computer-Aided Design, 4th International Conference, 2002

2001

Formally Analyzed Dynamic Synthesis of Hardware.

Kong Woei Susanto, Thomas F. Melham

J. Supercomput., 2001

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

2000

An analysis of errors in interactive proof attempts.

J. Stuart Aitken, Thomas F. Melham

Interact. Comput., 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

Proceedings of the Tools and Algorithms for Construction and Analysis of Systems, 2000

A Methodology for Large-Scale Hardware Verification.

Mark D. Aagaard, Robert B. Jones, Thomas F. Melham, John W. O'Leary, Carl-Johan H. Seger

Proceedings of the Formal Methods in Computer-Aided Design, Third International Conference, 2000

1999

Xs are for Trajectory Evaluation, Booleans are for Theorem Proving.

Mark D. Aagaard, Thomas F. Melham, John W. O'Leary

Proceedings of the Correct Hardware Design and Verification Methods, 1999

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

Dynamic Specialization of XC6200 FPGAs by Partial Evaluation.

Nicholas McKay, Thomas F. Melham, Kong Woei Susanto, Satnam Singh

Proceedings of the 6th IEEE Symposium on Field-Programmable Custom Computing Machines (FCCM '98), 1998

1996

Five Axioms of Alpha-Conversion.

Andrew D. Gordon, Thomas F. Melham

Proceedings of the Theorem Proving in Higher Order Logics, 9th International Conference, 1996

1994

A Mechanized Theory of the Pi-Calculus in HOL.

Thomas F. Melham

Nord. J. Comput., 1994

1993

The HOL Logic Extended with Quantification over Type Variables.

Thomas F. Melham

Formal Methods Syst. Des., 1993

Translating Dependent Type Theory into Higher Order Logic.

Bart Jacobs, Thomas F. Melham

Proceedings of the Typed Lambda Calculi and Applications, 1993

Higher Order Logic and Hardware Verification.

Thomas F. Melham

Cambridge Tracts in Theoretical Computer Science 31, Cambridge University Press, ISBN: 9780521417181, 1993

1991

A Package for Inductive Relation Definitions in HOL.

Thomas F. Melham

Proceedings of the 1991 International Workshop on the HOL Theorem Proving System and its Applications, 1991