default search action
Tom 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
2020 – today
- 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) - [c37]Avi Shaked
, Nan Messe
Modelling Tool Extension for Vulnerability Management. MoDELS (Companion) 2024: 56-60 - 2023
- [c36]Seung Hoon Park
A Formal CHERI-C Semantics for Verification. TACAS (1) 2023: 549-568 - 2022
- [j12]Natasha Yogananda Jeppu
Enhancing active model learning with equivalence checking using simulation relations. Formal Methods Syst. Des. 61(2): 164-197 (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
Position Paper: Towards a Hybrid Approach to Protect Against Memory Safety Vulnerabilities. SecDev 2022: 52-58 - [i15]Seung Hoon Park, Rekha R. Pai, Tom Melham:
A Formal CHERI-C Semantics for Verification. CoRR abs/2211.07511 (2022) - 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
End-to-End Formal Verification of a RISC-V Processor Extended with Capability Pointers. FMCAD 2021: 24-33 - [c31]Isaac Dunn
Exposing previously undetectable faults in deep neural networks. ISSTA 2021: 56-66 - [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
- [c30]Natasha Yogananda Jeppu
Learning Concise Models from Long Execution Traces. DAC 2020: 1-6 - [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
Learning Concise Models from Long Execution Traces. CoRR abs/2001.05230 (2020) - [i10]Isaac Dunn
Semantic Adversarial Perturbations using Learnt Representations. CoRR abs/2001.11055 (2020)
2010 – 2019
- 2019
- [c29]Sean Heelan, Tom Melham, Daniel Kroening
Gollum: Modular and Greybox Exploit Generation for Heap Overflows in Interpreters. CCS 2019: 1689-1706 - [i9]Isaac Dunn
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
DeepSynth: Program Synthesis for Automatic Task Segmentation in Deep Reinforcement Learning. CoRR abs/1911.10244 (2019) - 2018
- [j11]Lihao Liang
Effective Verification for Low-Level Software with Competing Interrupts. ACM Trans. Embed. Comput. Syst. 17(2): 36:1-36:26 (2018) - [c28]Lihao Liang, Paul E. McKenney, Daniel Kroening
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 - [p1]Tom Melham:
Symbolic Trajectory Evaluation. Handbook of Model Checking 2018: 831-870 - [i6]Sean Heelan, Tom Melham, Daniel Kroening:
Automatic Heap Layout Manipulation for Exploitation. CoRR abs/1804.08470 (2018) - 2017
- [c26]Rajdeep Mukherjee, Peter Schrammel
Lifting CDCL to Template-Based Abstract Domains for Program Verification. ATVA 2017: 307-326 - [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
- [j10]Peter Schrammel
Generating test case chains for reactive systems. Int. J. Softw. Tools Technol. Transf. 18(3): 319-334 (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
Equivalence Checking of a Floating-Point Unit Against a High-Level C Model. FM 2016: 551-558 - [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) - 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
Hardware Verification Using Software Analyzers. ISVLSI 2015: 7-12 - [c21]Rajdeep Mukherjee, Daniel Kroening
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
Chaining Test Cases for Reactive System Testing. ICTSS 2013: 133-148 - [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)
2000 – 2009
- 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 - 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
An industrially effective environment for formal hardware verification. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 24(9): 1381-1405 (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 - [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] - 2004
- [c12]Thomas F. Melham:
Integrating Model Checking and Theorem Proving in a Reflective Functional Language. IFM 2004: 36-39 - 2003
- [j7]Louise A. Dennis
The PROSPER toolkit. Int. J. Softw. Tools Technol. Transf. 4(2): 189-210 (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 - 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) - [e3]Tiziana Margaria
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] - 2000
- [j4]J. Stuart Aitken, Thomas F. Melham:
An analysis of errors in interactive proof attempts. Interact. Comput. 12(6): 565-586 (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
The PROSPER Toolkit. TACAS 2000: 78-92
1990 – 1999
- 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
- [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) - [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 - 1994
- [j2]Thomas F. Melham:
A Mechanized Theory of the Pi-Calculus in HOL. Nord. J. Comput. 1(1): 50-76 (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] - 1993
- [b1]Thomas F. Melham:
Higher Order Logic and Hardware Verification. Cambridge Tracts in Theoretical Computer Science 31, Cambridge University Press 1993, ISBN 9780521417181 - [j1]Thomas F. Melham:
The HOL Logic Extended with Quantification over Type Variables. Formal Methods Syst. Des. 3(1/2): 7-24 (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 - [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] - 1991
- [c1]Thomas F. Melham:
A Package for Inductive Relation Definitions in HOL. TPHOLs 1991: 350-357
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-11-07 20:29 CET 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: