Stop the war!Остановите войну!
for scientists:
default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDTom Melham
Person information
- affiliation: University of Oxford, Department of Computer Science, UK
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
Books and Theses
- 1993
[b1]Thomas F. Melham:
Higher Order Logic and Hardware Verification. Cambridge Tracts in Theoretical Computer Science 31, Cambridge University Press 1993, ISBN 9780521417181
Journal Articles
- 2024
- [j13]Hosein Hasanbeig, Natasha Yogananda Jeppu, Alessandro Abate, Tom Melham, Daniel Kroening:
Symbolic Task Inference in Deep Reinforcement Learning. J. Artif. Intell. Res. 80: 1099-1137 (2024) - 2022
- [j12]Natasha Yogananda Jeppu
, Tom Melham, Daniel Kroening:
Enhancing active model learning with equivalence checking using simulation relations. Formal Methods Syst. Des. 61(2): 164-197 (2022) - 2018
- [j11]Lihao Liang, Tom Melham, Daniel Kroening, Peter Schrammel, Michael Tautschnig:
Effective Verification for Low-Level Software with Competing Interrupts. ACM Trans. Embed. Comput. Syst. 17(2): 36:1-36:26 (2018) - 2016
- [j10]Peter Schrammel, Tom Melham, Daniel Kroening:
Generating test case chains for reactive systems. Int. J. Softw. Tools Technol. Transf. 18(3): 319-334 (2016) - 2006
- [j9]Jim Grundy, Thomas F. Melham, John W. O'Leary:
A reflective functional language for hardware design and theorem proving. J. Funct. Program. 16(2): 157-196 (2006) - 2005
- [j8]Carl-Johan H. Seger, Robert B. Jones, John W. O'Leary, Thomas F. Melham, Mark D. Aagaard, Clark W. Barrett, Don Syme:
An industrially effective environment for formal hardware verification. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 24(9): 1381-1405 (2005) - 2003
- [j7]Louise A. Dennis, Graham Collins, Michael Norrish, Richard J. Boulton, Konrad Slind, Thomas F. Melham:
The PROSPER toolkit. Int. J. Softw. Tools Technol. Transf. 4(2): 189-210 (2003) - 2001
- [j6]Robert B. Jones, John W. O'Leary, Carl-Johan H. Seger, Mark D. Aagaard, Thomas F. Melham:
Practical Formal Verification in Microprocessor Design. IEEE Des. Test Comput. 18(4): 16-25 (2001) - [j5]Kong Woei Susanto, Thomas F. Melham:
Formally Analyzed Dynamic Synthesis of Hardware. J. Supercomput. 19(1): 7-22 (2001) - 2000
- [j4]J. Stuart Aitken, Thomas F. Melham:
An analysis of errors in interactive proof attempts. Interact. Comput. 12(6): 565-586 (2000) - 1998
- [j3]J. Stuart Aitken, Philip D. Gray, Thomas F. Melham, Muffy Thomas:
Interactive Theorem Proving: An Empirical Study of User Activity. J. Symb. Comput. 25(2): 263-284 (1998) - 1994
- [j2]Thomas F. Melham:
A Mechanized Theory of the Pi-Calculus in HOL. Nord. J. Comput. 1(1): 50-76 (1994) - 1993
- [j1]Thomas F. Melham:
The HOL Logic Extended with Quantification over Type Variables. Formal Methods Syst. Des. 3(1/2): 7-24 (1993)
Conference and Workshop Papers
- 2023
- [c36]Seung Hoon Park, Rekha R. Pai, Tom Melham:
A Formal CHERI-C Semantics for Verification. TACAS (1) 2023: 549-568 - 2022
- [c35]Natasha Yogananda Jeppu, Tom Melham, Daniel Kroening:
Active Learning of Abstract System Models from Traces using Model Checking. DATE 2022: 100-103 - [c34]Kaled M. Alshmrany, Ahmed Bhayat, Franz Brauße, Lucas C. Cordeiro, Konstantin Korovin, Tom Melham, Mustafa A. Mustafa, Pierre Olivier, Giles Reger, Fedor Shmarov:
Position Paper: Towards a Hybrid Approach to Protect Against Memory Safety Vulnerabilities. SecDev 2022: 52-58 - 2021
- [c33]Mohammadhosein Hasanbeig, Natasha Yogananda Jeppu, Alessandro Abate, Tom Melham, Daniel Kroening:
DeepSynth: Automata Synthesis for Automatic Task Segmentation in Deep Reinforcement Learning. AAAI 2021: 7647-7656 - [c32]Dapeng Gao, Tom Melham:
End-to-End Formal Verification of a RISC-V Processor Extended with Capability Pointers. FMCAD 2021: 24-33 - [c31]Isaac Dunn, Hadrien Pouget, Daniel Kroening, Tom Melham:
Exposing previously undetectable faults in deep neural networks. ISSTA 2021: 56-66 - 2020
- [c30]Natasha Yogananda Jeppu, Thomas F. Melham, Daniel Kroening, John O'Leary:
Learning Concise Models from Long Execution Traces. DAC 2020: 1-6 - 2019
- [c29]Sean Heelan, Tom Melham, Daniel Kroening:
Gollum: Modular and Greybox Exploit Generation for Heap Overflows in Interpreters. CCS 2019: 1689-1706 - 2018
- [c28]Lihao Liang, Paul E. McKenney, Daniel Kroening, Tom Melham:
Verification of tree-based hierarchical read-copy update in the Linux kernel. DATE 2018: 61-66 - [c27]Sean Heelan, Tom Melham, Daniel Kroening:
Automatic Heap Layout Manipulation for Exploitation. USENIX Security Symposium 2018: 763-779 - 2017
- [c26]Rajdeep Mukherjee, Peter Schrammel, Leopold Haller, Daniel Kroening, Tom Melham:
Lifting CDCL to Template-Based Abstract Domains for Program Verification. ATVA 2017: 307-326 - 2016
- [c25]Rajdeep Mukherjee, Peter Schrammel, Daniel Kroening, Tom Melham:
Unbounded safety verification for hardware using software analyzers. DATE 2016: 1152-1155 - [c24]Rajdeep Mukherjee, Saurabh Joshi, Andreas Griesmayer, Daniel Kroening, Tom Melham:
Equivalence Checking of a Floating-Point Unit Against a High-Level C Model. FM 2016: 551-558 - 2015
- [c23]Daniel Kroening, Lihao Liang, Tom Melham, Peter Schrammel, Michael Tautschnig:
Effective verification of low-level software with nested interrupts. DATE 2015: 229-234 - [c22]Rajdeep Mukherjee, Daniel Kroening, Tom Melham:
Hardware Verification Using Software Analyzers. ISVLSI 2015: 7-12 - [c21]Rajdeep Mukherjee, Daniel Kroening, Tom Melham, Mandayam K. Srivas:
Equivalence Checking Using Trace Partitioning. ISVLSI 2015: 13-18 - 2013
- [c20]John W. O'Leary, Roope Kaivola, Tom Melham:
Relational STE and theorem proving for formal verification of industrial circuit designs. FMCAD 2013: 97-104 - [c19]Alex Horn, Michael Tautschnig, Celina G. Val, Lihao Liang, Tom Melham, Jim Grundy, Daniel Kroening:
Formal co-validation of low-level hardware/software interfaces. FMCAD 2013: 121-128 - [c18]Peter Schrammel, Tom Melham, Daniel Kroening:
Chaining Test Cases for Reactive System Testing. ICTSS 2013: 133-148 - 2009
- [c17]Zurab Khasidashvili, Gavriel Gavrielov, Tom Melham:
Assume-guarantee validation for STE properties within an SVA environment. FMCAD 2009: 108-115 - [c16]Ziyad Hanna, Thomas F. Melham:
A symbolic execution framework for algorithm-level modelling. HLDVT 2009: 94-99 - 2008
- [c15]Peter Böhm, Tom Melham:
A Refinement Approach to Design and Verification of On-Chip Communication Protocols. FMCAD 2008: 1-8 - 2007
- [c14]Sara Adams, Magnus Björk, Thomas F. Melham, Carl-Johan H. Seger:
Automatic Abstraction in Symbolic Trajectory Evaluation. FMCAD 2007: 127-135 - 2005
- [c13]Jim Grundy, Thomas F. Melham, Sava Krstic, Sean McLaughlin:
Tool Building Requirements for an API to First-Order Solvers. PDPAR@CAV 2005: 15-26 - 2004
- [c12]Thomas F. Melham:
Integrating Model Checking and Theorem Proving in a Reflective Functional Language. IFM 2004: 36-39 - 2003
- [c11]Kong Woei Susanto, Thomas F. Melham:
An AMBA-ARM7 Formal Verification Platform. ICFEM 2003: 48-67 - 2002
- [c10]Thomas F. Melham, Robert B. Jones:
Abstraction by Symbolic Indexing Transformations. FMCAD 2002: 1-18 - [c9]Thomas F. Melham:
PROSPER - An Investigation into Software Architecture for Embedded Proof Engines. FroCoS 2002: 193-206 - 2000
- [c8]Mark D. Aagaard, Robert B. Jones, Thomas F. Melham, John W. O'Leary, Carl-Johan H. Seger:
A Methodology for Large-Scale Hardware Verification. FMCAD 2000: 263-282 - [c7]Louise A. Dennis, Graham Collins, Michael Norrish, Richard J. Boulton, Konrad Slind, Graham Robinson, Michael J. C. Gordon, Thomas F. Melham:
The PROSPER Toolkit. TACAS 2000: 78-92 - 1999
- [c6]Mark D. Aagaard, Thomas F. Melham, John W. O'Leary:
Xs are for Trajectory Evaluation, Booleans are for Theorem Proving. CHARME 1999: 202-218 - 1998
- [c5]Nicholas McKay, Thomas F. Melham, Kong Woei Susanto, Satnam Singh:
Dynamic Specialization of XC6200 FPGAs by Partial Evaluation. FCCM 1998: 308-309 - 1996
- [c4]Andrew D. Gordon, Thomas F. Melham:
Five Axioms of Alpha-Conversion. TPHOLs 1996: 173-190 - 1993
- [c3]Bart Jacobs, Thomas F. Melham:
Translating Dependent Type Theory into Higher Order Logic. TLCA 1993: 209-229 - 1992
- [c2]Thomas F. Melham:
The HOL Logic Extended with Quantification over Type Variables. TPHOLs 1992: 3-17 - 1991
- [c1]Thomas F. Melham:
A Package for Inductive Relation Definitions in HOL. TPHOLs 1991: 350-357
Parts in Books or Collections
- 2018
- [p1]Tom Melham:
Symbolic Trajectory Evaluation. Handbook of Model Checking 2018: 831-870
Editorship
- 2005
- [e4]Joe Hurd, Thomas F. Melham:
Theorem Proving in Higher Order Logics, 18th International Conference, TPHOLs 2005, Oxford, UK, August 22-25, 2005, Proceedings. Lecture Notes in Computer Science 3603, Springer 2005, ISBN 3-540-28372-2 [contents] - 2001
- [e3]Tiziana Margaria, Thomas F. Melham:
Correct Hardware Design and Verification Methods, 11th IFIP WG 10.5 Advanced Research Working Conference, CHARME 2001, Livingston, Scotland, UK, September 4-7, 2001, Proceedings. Lecture Notes in Computer Science 2144, Springer 2001, ISBN 3-540-42541-1 [contents] - 1994
- [e2]Thomas F. Melham, Juanito Camilleri:
Higher Order Logic Theorem Proving and Its Applications, 7th International Workshop, Valletta, Malta, September 19-22, 1994, Proceedings. Lecture Notes in Computer Science 859, Springer 1994, ISBN 3-540-58450-1 [contents] - 1992
- [e1]Victoria Stavridou, Thomas F. Melham, Raymond T. Boute:
Theorem Provers in Circuit Design, Proceedings of the IFIP TC10/WG 10.2 International Conference on Theorem Provers in Circuit Design: Theory, Practice and Experience, Nijmegen, The Netherlands, 22-24 June 1992, Proceedings. IFIP Transactions A-10, North-Holland 1992, ISBN 0-444-89686-4 [contents]
Informal and Other Publications
- 2022
- [i15]Seung Hoon Park, Rekha R. Pai, Tom Melham:
A Formal CHERI-C Semantics for Verification. CoRR abs/2211.07511 (2022) - 2021
- [i14]Isaac Dunn, Hadrien Pouget, Daniel Kroening, Tom Melham:
Exposing Previously Undetectable Faults in Deep Neural Networks. CoRR abs/2106.00576 (2021) - [i13]Natasha Yogananda Jeppu, Tom Melham, Daniel Kroening:
Active Learning of Abstract System Models from Traces using Model Checking [Extended]. CoRR abs/2112.05990 (2021) - 2020
- [i12]Rajdeep Mukherjee, Saurabh Joshi, John O'Leary, Daniel Kroening, Tom Melham:
Hardware/Software Co-verification Using Path-based Symbolic Execution. CoRR abs/2001.01324 (2020) - [i11]Natasha Yogananda Jeppu, Tom Melham, Daniel Kroening, John O'Leary:
Learning Concise Models from Long Execution Traces. CoRR abs/2001.05230 (2020) - [i10]Isaac Dunn, Tom Melham, Daniel Kroening:
Semantic Adversarial Perturbations using Learnt Representations. CoRR abs/2001.11055 (2020) - 2019
- [i9]Isaac Dunn, Tom Melham, Daniel Kroening:
Generating Realistic Unrestricted Adversarial Inputs using Dual-Objective GAN Training. CoRR abs/1905.02463 (2019) - [i8]Andreas Tiemeyer, Tom Melham, Daniel Kroening, John O'Leary:
CREST: Hardware Formal Verification with ANSI-C Reference Specifications. CoRR abs/1908.01324 (2019) - [i7]Mohammadhosein Hasanbeig, Natasha Yogananda Jeppu, Alessandro Abate, Tom Melham, Daniel Kroening:
DeepSynth: Program Synthesis for Automatic Task Segmentation in Deep Reinforcement Learning. CoRR abs/1911.10244 (2019) - 2018
- [i6]Sean Heelan, Tom Melham, Daniel Kroening:
Automatic Heap Layout Manipulation for Exploitation. CoRR abs/1804.08470 (2018) - 2017
- [i5]Rajdeep Mukherjee, Peter Schrammel, Leopold Haller, Daniel Kroening, Tom Melham:
Lifting CDCL to Template-based Abstract Domains for Program Verification. CoRR abs/1707.02011 (2017) - 2016
- [i4]Rajdeep Mukherjee, Saurabh Joshi, Andreas Griesmayer, Daniel Kroening, Tom Melham:
Equivalence Checking a Floating-point Unit against a High-level C Model (Extended Version). CoRR abs/1609.00169 (2016) - [i3]Lihao Liang, Paul E. McKenney, Daniel Kroening, Tom Melham:
Verification of the Tree-Based Hierarchical Read-Copy Update in the Linux Kernel. CoRR abs/1610.03052 (2016) - 2013
- [i2]Peter Schrammel, Tom Melham, Daniel Kroening:
Chaining Test Cases for Reactive System Testing (extended version). CoRR abs/1306.3882 (2013) - [i1]Tom Melham, Raphael Cohn, Ian Childs:
On the Semantics of ReFLect as a Basis for a Reflective Theorem Prover. CoRR abs/1309.5742 (2013)
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from 
to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the 
of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from 
, 
, and 
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from 
.
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-08-10 01:21 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
