Tom Melham : Publications

Active Learning of Abstract System Models from Traces using Model Checking

Natasha Yogananda Jeppu‚ Tom Melham and Daniel Kroening

In Cristiana Bolchini‚ Ingrid Verbauwhede and Ioana Vatajelu, editors, 2022 Design‚ Automation & Test in Europe Conference & Exhibition‚ DATE 2022‚ Antwerp‚ Belgium‚ March 14−23‚ 2022. Pages 100–103. IEEE. March, 2022.

Details about Active Learning of Abstract System Models from Traces using Model Checking | BibTeX data for Active Learning of Abstract System Models from Traces using Model Checking | DOI (10.23919/DATE54114.2022.9774595) | Download (pdf) of Active Learning of Abstract System Models from Traces using Model Checking

Exposing Previously Undetectable Faults in Deep Neural Networks

Isaac Dunn‚ Hadrien Pouget‚ Daniel Kroening and Tom Melham

In Cristian Cadar and Xiangyu Zhang, editors, ISSTA 2021: Proceedings of the 30th ACM SIGSOFT International Symposium on Software Testing and Analysis. Vol. arXiv:2106.00576 [cs.LG]. Pages 56–66. June, 2021.

Details about Exposing Previously Undetectable Faults in Deep Neural Networks | BibTeX data for Exposing Previously Undetectable Faults in Deep Neural Networks | DOI (10.1145/3460319.3464801) | Link to Exposing Previously Undetectable Faults in Deep Neural Networks

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

Natasha Yogananda Jeppu‚ Tom Melham and Daniel Kroening

In arXiv Computing Research Repository. Vol. arXiv:2112.05990 [cs.FL]. December, 2021.

Details about Active Learning of Abstract System Models from Traces using Model Checking [Extended] | BibTeX data for Active Learning of Abstract System Models from Traces using Model Checking [Extended] | Link to Active Learning of Abstract System Models from Traces using Model Checking [Extended]

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

Dapeng Gao and Tom Melham

In Ruzica Piskac and Michael W. Whalen, editors, Proceedings of the 21st Conference on Formal Methods in Computer−Aided Design –− FMCAD 2021. Vol. 2. Pages 24–33. TUI Wien Academic Press. October, 2021.

Details about End−to−End Formal Verification of a RISC−V Processor Extended with Capability Pointers | BibTeX data for End−to−End Formal Verification of a RISC−V Processor Extended with Capability Pointers | DOI (10.34727/2021/isbn.978-3-85448-046-4_10) | Download (pdf) of End−to−End Formal Verification of a RISC−V Processor Extended with Capability Pointers

Towards a Hybrid Approach to Protect Against Memory Safety Vulnerabilities

Kaled Alshmrany‚ Ahmed Bhayat‚ Lucas Cordeiro‚ Konstantin Korovin‚ Tom Melham‚ Mustafa A. Mustafa‚ Pierre Olivier‚ Giles Reger and Fedor Shmarov

In TechRxiv. 2021.

Preprint

Details about Towards a Hybrid Approach to Protect Against Memory Safety Vulnerabilities | BibTeX data for Towards a Hybrid Approach to Protect Against Memory Safety Vulnerabilities | Link to Towards a Hybrid Approach to Protect Against Memory Safety Vulnerabilities

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

Mohammadhosein Hasanbeig‚ Natasha Yogananda Jeppu‚ Alessandro Abate‚ Tom Melham and Daniel Kroening

In 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. AAAI Press. 2021.

Details about DeepSynth: Automata Synthesis for Automatic Task Segmentation in Deep Reinforcement Learning | BibTeX data for DeepSynth: Automata Synthesis for Automatic Task Segmentation in Deep Reinforcement Learning | Link to DeepSynth: Automata Synthesis for Automatic Task Segmentation in Deep Reinforcement Learning

Evaluating Robustness to Context−Sensitive Feature Perturbations of Different Granularities

Isaac Dunn‚ Laura Hanu‚ Hadrien Pouget‚ Daniel Kroening and Tom Melham

In arXiv Computing Research Repository. Vol. arXiv:2001.11055 [cs.CV]. June, 2020.

Details about Evaluating Robustness to Context−Sensitive Feature Perturbations of Different Granularities | BibTeX data for Evaluating Robustness to Context−Sensitive Feature Perturbations of Different Granularities | Link to Evaluating Robustness to Context−Sensitive Feature Perturbations of Different Granularities

Investigating Distributional Robustness: Semantic Perturbations Using Generative Models

Isaac Dunn‚ Laura Hanu‚ Hadrien Pouget‚ Daniel Kroening and Tom Melham

In arXiv Computing Research Repository. Vol. arXiv:2001.11055 [cs.CV]. June, 2020.

Details about Investigating Distributional Robustness: Semantic Perturbations Using Generative Models | BibTeX data for Investigating Distributional Robustness: Semantic Perturbations Using Generative Models | Link to Investigating Distributional Robustness: Semantic Perturbations Using Generative Models

Automated decision−making in the public sector

Rebecca Williams and Thomas Melham

In Practical Law Public Sector. December, 2020.

Resource ID w 028 6934

Details about Automated decision−making in the public sector | BibTeX data for Automated decision−making in the public sector | Download (pdf) of Automated decision−making in the public sector

Recalibrating classifiers for interpretable abusive content detection

Bertie Vidgen‚ Sam Staton‚ Scott Hale‚ Ohad Kammar‚ Helen Margetts‚ Tom Melham and Marcin Szymczak

In Proceedings of the Fourth Workshop on Natural Language Processing and Computational Social Science. Pages 132–138. Association for Computational Linguistics. November, 2020.

Details about Recalibrating classifiers for interpretable abusive content detection | BibTeX data for Recalibrating classifiers for interpretable abusive content detection | DOI (10.18653/v1/2020.nlpcss-1.14) | Link to Recalibrating classifiers for interpretable abusive content detection

Hardware/Software Co−verification Using Path−based Symbolic Execution

Rajdeep Mukherjee‚ Saurahb Joshi‚ John O'Leary‚ Daniel Kroening and Tom Melham

In arXiv Computing Research Repository. Vol. arXiv:2001.01324 [cs.FL]. January, 2020.

Details about Hardware/Software Co−verification Using Path−based Symbolic Execution | BibTeX data for Hardware/Software Co−verification Using Path−based Symbolic Execution | Link to Hardware/Software Co−verification Using Path−based Symbolic Execution

Learning Concise Models from Long Execution Traces

Natasha Yogananda Jeppu‚ Tom Melham‚ Daniel Kroening and John O'Leary

In arXiv Computing Research Repository. Vol. arXiv:2001.05230 [cs.FL]. January, 2020.

Details about Learning Concise Models from Long Execution Traces | BibTeX data for Learning Concise Models from Long Execution Traces | Link to Learning Concise Models from Long Execution Traces

Learning Concise Models from Long Execution Traces

Natasha Yogananda Jeppu‚ Thomas Melham‚ Daniel Kroening and John O'Leary

In 57th ACM/IEEE Design Automation Conference‚ DAC 2020‚ San Francisco‚ CA‚ USA‚ July 20–24‚ 2020. Pages 1–6. IEEE Press. 2020.

Details about Learning Concise Models from Long Execution Traces | BibTeX data for Learning Concise Models from Long Execution Traces | DOI (10.1109/DAC18072.2020.9218613)

CREST: Hardware Formal Verification with ANSI−C Reference Specifications

Andreas Tiemeyer‚ Tom Melham‚ Daniel Kroening and John O'Leary

In arXiv Computing Research Repository. Vol. arXiv:1908.01324 [cs.PL]. August, 2019.

Details about CREST: Hardware Formal Verification with ANSI−C Reference Specifications | BibTeX data for CREST: Hardware Formal Verification with ANSI−C Reference Specifications | Link to CREST: Hardware Formal Verification with ANSI−C Reference Specifications

DeepSynth: Program Synthesis for Automatic Task Segmentation in Deep Reinforcement Learning

Mohammadhosein Hasanbeig‚ Natasha Yogananda Jeppu‚ Alessandro Abate‚ Tom Melham and Daniel Kroening

In arXiv Computing Research Repository. Vol. arXiv:1911.10244 [cs.LG]. November, 2019.

Details about DeepSynth: Program Synthesis for Automatic Task Segmentation in Deep Reinforcement Learning | BibTeX data for DeepSynth: Program Synthesis for Automatic Task Segmentation in Deep Reinforcement Learning | Link to DeepSynth: Program Synthesis for Automatic Task Segmentation in Deep Reinforcement Learning

Adaptive Generation of Unrestricted Adversarial Inputs

Isaac Dunn‚ Hadrien Pouget‚ Tom Melham and Daniel Kroening

In arXiv Computing Research Repository. Vol. arXiv:1905.02463 [cs.LG]. October, 2019.

Details about Adaptive Generation of Unrestricted Adversarial Inputs | BibTeX data for Adaptive Generation of Unrestricted Adversarial Inputs | Link to Adaptive Generation of Unrestricted Adversarial Inputs

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

Sean Heelan‚ Tom Melham and Daniel Kroening

In Lorenzo Cavallaro‚ Johannes Kinder‚ XiaoFeng Wang and Jonathan Katz, editors, Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security‚ CCS 2019‚ London‚ UK‚ November 11−15‚ 2019. Pages 1689–1706. ACM. 2019.

Details about Gollum: Modular and Greybox Exploit Generation for Heap Overflows in Interpreters | BibTeX data for Gollum: Modular and Greybox Exploit Generation for Heap Overflows in Interpreters | DOI (10.1145/3319535.3354224) | Download (pdf) of Gollum: Modular and Greybox Exploit Generation for Heap Overflows in Interpreters

Automatic Heap Layout Manipulation for Exploitation

Sean Heelan‚ Tom Melham and Daniel Kroening

In arXiv Computing Research Repository. Vol. arXiv:1804.08470 [cs.CR]. April, 2018.

Details about Automatic Heap Layout Manipulation for Exploitation | BibTeX data for Automatic Heap Layout Manipulation for Exploitation | Link to Automatic Heap Layout Manipulation for Exploitation

Verification of Tree−Based Hierarchical Read−Copy Update in the Linux Kernel

Lihao Liang‚ Paul E. McKenney‚ Daniel Kroening and Tom Melham

In Jan Madsen and Ayse K. Coskun, editors, 2018 Design‚ Automation & Test in Europe Conference & Exhibition‚ DATE 2018‚ Dresden‚ Germany‚ March 19–23‚ 2018. Pages 61–66. European Design and Automation Association. 2018.

Details about Verification of Tree−Based Hierarchical Read−Copy Update in the Linux Kernel | BibTeX data for Verification of Tree−Based Hierarchical Read−Copy Update in the Linux Kernel | DOI (10.23919/DATE.2018.8341980) | Download (pdf) of Verification of Tree−Based Hierarchical Read−Copy Update in the Linux Kernel

Automatic Heap Layout Manipulation for Exploitation

Sean Heelan‚ Tom Melham and Daniel Kroening

In William Enck and Adrienne Porter Felt, editors, 27th USENIX Security Symposium‚ USENIX Security 18: Baltimore‚ MD‚ USA‚ August 15–17‚ 2018. Pages 763–779. USENIX Association. 2018.

Details about Automatic Heap Layout Manipulation for Exploitation | BibTeX data for Automatic Heap Layout Manipulation for Exploitation | Download (pdf) of Automatic Heap Layout Manipulation for Exploitation

Symbolic Trajectory Evaluation

Tom Melham

In Edmund M. Clarke‚ Thomas A. Henzinger‚ Helmut Veith and Roderick Bloem, editors, Handbook of Model Checking. Chapter 25. Pages 831–870. Springer International Publishing. 2018.

Details about Symbolic Trajectory Evaluation | BibTeX data for Symbolic Trajectory Evaluation | DOI (10.1007/978-3-319-10575-8_25)

Lifting CDCL to Template−Based Abstract Domains for Program Verification

Rajdeep Mukherjee‚ Peter Schrammel‚ Leopold Haller‚ Daniel Kroening and Tom Melham

In arXiv Computing Research Repository. Vol. arXiv:1707.02011 [cs.LO]. July, 2017.

Details about Lifting CDCL to Template−Based Abstract Domains for Program Verification | BibTeX data for Lifting CDCL to Template−Based Abstract Domains for Program Verification | Link to Lifting CDCL to Template−Based Abstract Domains for Program Verification

Effective Verification for Low−Level Software with Competing Interrupts

Lihao Liang‚ Tom Melham‚ Daniel Kroening‚ Peter Schrammel and Michael Tautschnig

In ACM Transactions on Embedded Computing Systems. Vol. 17. No. 2. Pages 36:1–36:26. December, 2017.

Details about Effective Verification for Low−Level Software with Competing Interrupts | BibTeX data for Effective Verification for Low−Level Software with Competing Interrupts | DOI (10.1145/3147432) | Download (pdf) of Effective Verification for Low−Level Software with Competing Interrupts

Lifting CDCL to Template−Based Abstract Domains for Program Verification

Rajdeep Mukherjee‚ Peter Schrammel‚ Leopold Haller‚ Daniel Kroening and Tom Melham

In Deepak D'Souza and K. Narayan Kumar, editors, Automated Technology for Verification and Analysis: 15th International Symposium‚ ATVA 2017‚ Pune‚ India‚ October 3−6‚ 2017‚ Proceedings. Vol. 10482 of Lecture Notes in Computer Science. Pages 307–326. Springer‚ Cham. 2017.

Details about Lifting CDCL to Template−Based Abstract Domains for Program Verification | BibTeX data for Lifting CDCL to Template−Based Abstract Domains for Program Verification | DOI (10.1007/978-3-319-68167-2_21) | Download (pdf) of Lifting CDCL to Template−Based Abstract Domains for Program Verification

Equivalence Checking a Floating−point Unit against a High−level C Model: Extended Version

Rajdeep Mukherjee‚ Saurabh Joshi‚ Andreas Griesmayer‚ Daniel Kroening and Tom Melham

In arXiv Computing Research Repository. Vol. arXiv:1609.00169 [cs.SE]. September, 2016.

Details about Equivalence Checking a Floating−point Unit against a High−level C Model: Extended Version | BibTeX data for Equivalence Checking a Floating−point Unit against a High−level C Model: Extended Version

Generating test case chains for reactive systems

Peter Schrammel‚ Tom Melham and Daniel Kroening

In International Journal on Software Tools for Technology Transfer. Vol. 18. No. 3. Pages 319–334. June, 2016.

Details about Generating test case chains for reactive systems | BibTeX data for Generating test case chains for reactive systems | DOI (10.1007/s10009-014-0358-6) | Download (pdf) of Generating test case chains for reactive systems

Verification of the Tree−Based Hierarchical Read−Copy Update in the Linux Kernel

Lihao Liang‚ Paul E. McKenney‚ Daniel Kroening and Tom Melham

In arXiv Computing Research Repository. Vol. arXiv:1610:03052 [cs.LO]. October, 2016.

Details about Verification of the Tree−Based Hierarchical Read−Copy Update in the Linux Kernel | BibTeX data for Verification of the Tree−Based Hierarchical Read−Copy Update in the Linux Kernel

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

Rajdeep Mukherjee‚ Saurabh Joshi‚ Andreas Griesmayer‚ Daniel Kroening and Tom Melham

In John S. Fitzgerald‚ Constance L. Heitmeyer‚ Stefania Gnesi and Anna Philippou, editors, FM 2016: Formal Methods − 21st International Symposium‚ Limassol‚ Cyprus‚ November 9−11‚ 2016‚ Proceedings. Vol. 9995 of Lecture Notes in Computer Science. Pages 551–558. Springer−Verlag. 2016.

Details about Equivalence Checking of a Floating−Point Unit Against a High−Level C Model | BibTeX data for Equivalence Checking of a Floating−Point Unit Against a High−Level C Model | DOI (10.1007/978-3-319-48989-6_33)

Unbounded safety verification for hardware using software analyzers

Rajdeep Mukherjee‚ Peter Schrammel‚ Daniel Kroening and Tom Melham

In Luca Fanucci and Jürgen Teich, editors, 2016 Design‚ Automation & Test in Europe Conference & Exhibition‚ DATE 2016‚ Dresden‚ Germany‚ March 14–18‚ 2016. Pages 1152–1155. European Design and Automation Association. 2016.

Details about Unbounded safety verification for hardware using software analyzers | BibTeX data for Unbounded safety verification for hardware using software analyzers | DOI (10.3850/9783981537079_0274) | Download (pdf) of Unbounded safety verification for hardware using software analyzers

Effective Verification of Low−Level Software with Nested Interrupts

Daniel Kroening‚ Lihao Liang‚ Tom Melham‚ Peter Schrammel and Michael Tautschnig

In Wolfgang Nebel and David Atienza, editors, Proceedings of the 2015 Design‚ Automation & Test in Europe Conference & Exhibition‚ DATE 2015‚ Grenoble‚ France‚ March 9−13‚ 2015. Pages 229–234. EDA Consortium. 2015.

Details about Effective Verification of Low−Level Software with Nested Interrupts | BibTeX data for Effective Verification of Low−Level Software with Nested Interrupts | Download (pdf) of Effective Verification of Low−Level Software with Nested Interrupts

Equivalence Checking Using Trace Partitioning

Rajdeep Mukherjee‚ Daniel Kroening‚ Tom Melham and Mandayam K. Srivas

In 2015 IEEE Computer Society Annual Symposium on VLSI‚ ISVLSI 2015‚ Montpellier‚ France‚ July 8−10‚ 2015. Pages 13–18. IEEE Computer Society. 2015.

Details about Equivalence Checking Using Trace Partitioning | BibTeX data for Equivalence Checking Using Trace Partitioning | DOI (10.1109/ISVLSI.2015.110)

Hardware Verification Using Software Analyzers

Rajdeep Mukherjee‚ Daniel Kroening and Tom Melham

In 2015 IEEE Computer Society Annual Symposium on VLSI‚ ISVLSI 2015‚ Montpellier‚ France‚ July 8−10‚ 2015. Pages 7–12. IEEE Computer Society. 2015.

Details about Hardware Verification Using Software Analyzers | BibTeX data for Hardware Verification Using Software Analyzers | DOI (10.1109/ISVLSI.2015.107)

Problem Solving for the 21st Century: Efficient Solvers for Satisfiability Modulo Theories

Clark Barrett‚ Daniel Kroening and Tom Melham

No. 3. London Mathematical Society and the Smith Institute for Industrial Mathematics and System Engineering. June, 2014.

Details about Problem Solving for the 21st Century: Efficient Solvers for Satisfiability Modulo Theories | BibTeX data for Problem Solving for the 21st Century: Efficient Solvers for Satisfiability Modulo Theories

On the Semantics of ReFLect as a Basis for a Reflective Theorem Prover

Tom Melham‚ Raphael Cohn and Ian Childs

In arXiv Computing Research Repository. Vol. arXiv:1309.5742 [cs.LO]. September, 2013.

Details about On the Semantics of ReFLect as a Basis for a Reflective Theorem Prover | BibTeX data for On the Semantics of ReFLect as a Basis for a Reflective Theorem Prover | Link to On the Semantics of ReFLect as a Basis for a Reflective Theorem Prover

Modelling‚ abstraction‚ and computation in systems biology: A view from computer science

Tom Melham

In Progress in Biophysics and Molecular Biology. Vol. 111. No. 2−3. Pages 129–136. April, 2013.

Focussed Issue: Conceptual Foundations of Systems Biology

Details about Modelling‚ abstraction‚ and computation in systems biology: A view from computer science | BibTeX data for Modelling‚ abstraction‚ and computation in systems biology: A view from computer science | DOI (10.1016/j.pbiomolbio.2012.08.015)

Chaining Test Cases for Reactive System Testing (extended version)

Peter Schrammel‚ Tom Melham and Daniel Kroening

In arXiv Computing Research Repository. Vol. arXiv:1306.3882 [cs.SE]. November, 2013.

Details about Chaining Test Cases for Reactive System Testing (extended version) | BibTeX data for Chaining Test Cases for Reactive System Testing (extended version) | Link to Chaining Test Cases for Reactive System Testing (extended version)

Chaining Test Cases for Reactive System Testing

Peter Schrammel‚ Tom Melham and Daniel Kroening

In Hüsnü Yenigün‚ Cemal Yilmaz and Andreas Ulrich, editors, Testing Software and Systems − 25th IFIP WG 6.1 International Conference‚ ICTSS 2013‚ Istanbul‚ Turkey‚ November 13−15‚ 2013‚ Proceedings. Vol. 8254 of Lecture Notes in Computer Science. Pages 133–148. Springer Verlag. November, 2013.

Details about Chaining Test Cases for Reactive System Testing | BibTeX data for Chaining Test Cases for Reactive System Testing | DOI (10.1007/978-3-642-41707-8_9) | Download (pdf) of Chaining Test Cases for Reactive System Testing

Formal Co−Validation of Low−Level Hardware/Software Interfaces

Alex Horn‚ Michael Tautschnig‚ Celina Val‚ Lihao Liang‚ Tom Melham‚ Jim Grundy and Daniel Kroening

In Barbara Jobstmann and Sandip Ray, editors, FMCAD 2013: Formal Methods in Computer−Aided Design: Portland‚ Oregon‚ USA‚ 20–23 October 2013. Pages 121–128. IEEE. 2013.

Details about Formal Co−Validation of Low−Level Hardware/Software Interfaces | BibTeX data for Formal Co−Validation of Low−Level Hardware/Software Interfaces | DOI (10.1109/FMCAD.2013.6679400) | Download (pdf) of Formal Co−Validation of Low−Level Hardware/Software Interfaces

Relational STE and Theorem Proving for Formal Verification of Industrial Circuit Designs

John O'Leary‚ Roope Kaivola and Tom Melham

In Barbara Jobstmann and Sandip Ray, editors, FMCAD 2013: Formal Methods in Computer−Aided Design: Portland‚ Oregon‚ USA‚ 20–23 October 2013. Pages 97–104. IEEE. 2013.

Details about Relational STE and Theorem Proving for Formal Verification of Industrial Circuit Designs | BibTeX data for Relational STE and Theorem Proving for Formal Verification of Industrial Circuit Designs | DOI (10.1109/FMCAD.2013.6679397) | Download (pdf) of Relational STE and Theorem Proving for Formal Verification of Industrial Circuit Designs

A Symbolic Execution Framework for Algorithm−Level Modelling

Ziyad Hanna and Tom Melham

In Priyank Kalla and Prabhat Mishra, editors, High Level Design Validation and Test Workshop‚ 2009. HLDVT 2009.. Pages 94–99. IEEE. 2009.

Details about A Symbolic Execution Framework for Algorithm−Level Modelling | BibTeX data for A Symbolic Execution Framework for Algorithm−Level Modelling | DOI (10.1109/HLDVT.2009.5340168) | Download (pdf) of A Symbolic Execution Framework for Algorithm−Level Modelling

Assume−Guarantee Validation for STE Properties within an SVA Environment

Zurab Khasidashvili‚ Gavriel Gavrielov and Tom Melham

In Armin Biere and Carl Pixley, editors, Proceedings of 9th International Conference: 2009 Formal Methods in Computer−Aided Design: FMCAD 2009. Pages 108–115. IEEE. 2009.

Details about Assume−Guarantee Validation for STE Properties within an SVA Environment | BibTeX data for Assume−Guarantee Validation for STE Properties within an SVA Environment | DOI (10.1109/FMCAD.2009.5351133) | Download (pdf) of Assume−Guarantee Validation for STE Properties within an SVA Environment

Design and Verification of On−Chip Communication Protocols

Peter Böhm and Tom Melham

No. RR−08−05. Oxford University Computing Laboratory. April, 2008.

Details about Design and Verification of On−Chip Communication Protocols | BibTeX data for Design and Verification of On−Chip Communication Protocols | Download (pdf) of Design and Verification of On−Chip Communication Protocols

Design and Verification of On−Chip Communication Protocols

Peter Böhm and Tom Melham

In Gordon J. Pace and Satnam Singh, editors, Seventh International Workshop on Designing Correct Circuits: Budapest‚ 29–30 March 2008: Participants' Proceedings. Pages 15–29. ETAPS 2008. March, 2008.

A Satellite Event of the ETAPS 2008 group of conferences

Details about Design and Verification of On−Chip Communication Protocols | BibTeX data for Design and Verification of On−Chip Communication Protocols | Download (pdf) of Design and Verification of On−Chip Communication Protocols

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

Peter Böhm and Tom Melham

In Alessandro Cimatti and Robert B. Jones, editors, 2008 Formal Methods in Computer Aided Design: Portland‚ Oregon‚ USA: 17–20 November 2008. Pages 136–143. IEEE. 2008.

Details about A Refinement Approach to Design and Verification of On−Chip Communication Protocols | BibTeX data for A Refinement Approach to Design and Verification of On−Chip Communication Protocols | DOI (10.1109/FMCAD.2008.ECP.22) | Download (pdf) of A Refinement Approach to Design and Verification of On−Chip Communication Protocols

Early Validation of Computer Microarchitecture with Algorithm Level Models

Ziyad Hanna and Tom Melham

In Andreas Prinz, editor, Proceedings of ASM'07: The 14th International Abstract State Machines Workshop. 2007.

Published electronically

Details about Early Validation of Computer Microarchitecture with Algorithm Level Models | BibTeX data for Early Validation of Computer Microarchitecture with Algorithm Level Models | Download (pdf) of Early Validation of Computer Microarchitecture with Algorithm Level Models

Automatic Abstraction in Symbolic Trajectory Evaluation

Sara Adams‚ Magnus Björk‚ Tom Melham and Carl−Johan Seger

In Jason Baumgartner and Mary Sheeran, editors, Formal Methods in Computer Aided Design: FMCAD 2007: November 11–14 2007‚ Austin‚ Texas‚ USA. Pages 127–135. IEEE Computer Society. 2007.

Details about Automatic Abstraction in Symbolic Trajectory Evaluation | BibTeX data for Automatic Abstraction in Symbolic Trajectory Evaluation | DOI (10.1109/FAMCAD.2007.27) | Download (pdf) of Automatic Abstraction in Symbolic Trajectory Evaluation

A Reflective Functional Language for Hardware Design and Theorem Proving

Jim Grundy‚ Tom Melham and John O'Leary

In Journal of Functional Programming. Vol. 16. No. 2. Pages 157–196. March, 2006.

Details about A Reflective Functional Language for Hardware Design and Theorem Proving | BibTeX data for A Reflective Functional Language for Hardware Design and Theorem Proving | DOI (10.1017/S0956796805005757) | Download (pdf) of A Reflective Functional Language for Hardware Design and Theorem Proving

A Functional HDL in ReFLect

Tom Melham and John O'Leary

In Mary Sheeran and Tom Melham, editors, Sixth International Workshop on Designing Correct Circuits: Vienna‚ 25–26 March 2006: Participants' Proceedings. ETAPS 2006. March, 2006.

A Satellite Event of the ETAPS 2006 group of conferences

Details about A Functional HDL in ReFLect | BibTeX data for A Functional HDL in ReFLect | Download (pdf) of A Functional HDL in ReFLect

Sixth International Workshop on Designing Correct Circuits: Vienna‚ 25–26 March 2006: Participants' Proceedings

Mary Sheeran and Tom Melham, editors

A Satellite Event of the ETAPS 2006 group of conferences

Details about Sixth International Workshop on Designing Correct Circuits: Vienna‚ 25–26 March 2006: Participants' Proceedings | BibTeX data for Sixth International Workshop on Designing Correct Circuits: Vienna‚ 25–26 March 2006: Participants' Proceedings | Download (pdf) of Sixth International Workshop on Designing Correct Circuits: Vienna‚ 25–26 March 2006: Participants' Proceedings

Tool Building Requirements for an API to First−Order Solvers

Jim Grundy‚ Tom Melham‚ Sava Krstić and Sean McLaughlin

In Electronic Notes in Theoretical Computer Science. Vol. 144. No. 2. Pages 15–26. January, 2006.

Details about Tool Building Requirements for an API to First−Order Solvers | BibTeX data for Tool Building Requirements for an API to First−Order Solvers | DOI (10.1016/j.entcs.2005.12.003) | Download (pdf) of Tool Building Requirements for an API to First−Order Solvers

An Industrially Effective Environment for Formal Hardware Verification

Carl−Johan H. Seger‚ Robert B. Jones‚ John W. O'Leary‚ Tom Melham‚ Mark D. Aagaard‚ Clark Barrett and Don Syme

In IEEE Transactions on Computer−Aided Design of Integrated Circuits and Systems. Vol. 24. No. 9. Pages 1381–1405. September, 2005.

Details about An Industrially Effective Environment for Formal Hardware Verification | BibTeX data for An Industrially Effective Environment for Formal Hardware Verification | DOI (10.1109/TCAD.2005.850814) | Download (pdf) of An Industrially Effective Environment for Formal Hardware Verification

Theorem Proving in Higher Order Logics: 18th International Conference‚ TPHOLs 2005: Oxford‚ UK‚ August 22–25‚ 2005: Proceedings

Joe Hurd and Tom Melham, editors

Details about Theorem Proving in Higher Order Logics: 18th International Conference‚ TPHOLs 2005: Oxford‚ UK‚ August 22–25‚ 2005: Proceedings | BibTeX data for Theorem Proving in Higher Order Logics: 18th International Conference‚ TPHOLs 2005: Oxford‚ UK‚ August 22–25‚ 2005: Proceedings | DOI (10.1007/11541868) | Link to Theorem Proving in Higher Order Logics: 18th International Conference‚ TPHOLs 2005: Oxford‚ UK‚ August 22–25‚ 2005: Proceedings

Automatic Symbolic Indexing Methods for Formal Verification on a Symbolic Lattice Domain

Thomas F. Melham and Robert B. Jones

June, 2004.

US Patent 7‚310‚790

Details about Automatic Symbolic Indexing Methods for Formal Verification on a Symbolic Lattice Domain | BibTeX data for Automatic Symbolic Indexing Methods for Formal Verification on a Symbolic Lattice Domain

Fifth International Workshop on Designing Correct Circuits: Barcelona‚ 27–28 March 2004: Participants' Proceedings

Tom Melham and Mary Sheeran, editors

A Satellite Event of the ETAPS 2004 group of conferences

Details about Fifth International Workshop on Designing Correct Circuits: Barcelona‚ 27–28 March 2004: Participants' Proceedings | BibTeX data for Fifth International Workshop on Designing Correct Circuits: Barcelona‚ 27–28 March 2004: Participants' Proceedings | Download (pdf) of Fifth International Workshop on Designing Correct Circuits: Barcelona‚ 27–28 March 2004: Participants' Proceedings

Integrating Model Checking and Theorem Proving in a Reflective Functional Language

Tom Melham

In Eerke A. Boiten‚ John Derrick and Graeme Smith, editors, Integrated Formal Methods: 4th International Conference‚ IFM 2004: Canterbury‚ UK‚ April 4–7‚ 2004: Proceedings. Vol. 2999 of Lecture Notes in Computer Science. Pages 36–39. Springer−Verlag. 2004.

Details about Integrating Model Checking and Theorem Proving in a Reflective Functional Language | BibTeX data for Integrating Model Checking and Theorem Proving in a Reflective Functional Language | Download (pdf) of Integrating Model Checking and Theorem Proving in a Reflective Functional Language

The PROSPER toolkit

Louise A. Dennis‚ Graham Collins‚ Michael Norrish‚ Richard J. Boulton‚ Konrad Slind and Thomas F. Melham

In International Journal on Software Tools for Technology Transfer. Vol. 4. No. 2. Pages 189–210. February, 2003.

Details about The PROSPER toolkit | BibTeX data for The PROSPER toolkit | DOI (10.1007/s100090200076) | Link to The PROSPER toolkit

A Reflective Functional Language for Hardware Design and Theorem Proving

Jim Grundy‚ Tom Melham and John O'Leary

No. PRG−RR−03−16. Programming Research Group‚ Oxford University Computing Laboratory. October, 2003.

Details about A Reflective Functional Language for Hardware Design and Theorem Proving | BibTeX data for A Reflective Functional Language for Hardware Design and Theorem Proving | Download (pdf) of A Reflective Functional Language for Hardware Design and Theorem Proving

Abstract: Experience with Practical Formal Verification at an Industrial Scale

Tom Melham

In Clare Dixon, editor, Proceedings of the Tenth Workshop on Automated Reasoning: Bridging the Gap between Theory and Practice: 15th–16th April 2003: Liverpool. Pages 1–2. Department of Computer Science‚ University of Liverpool. 2003.

Details about Abstract: Experience with Practical Formal Verification at an Industrial Scale | BibTeX data for Abstract: Experience with Practical Formal Verification at an Industrial Scale | Download (pdf) of Abstract: Experience with Practical Formal Verification at an Industrial Scale

An AMBA−ARM7 Formal Verification Platform

Kong Woei Susanto and Tom Melham

In Jin Song Dong and Jim Woodcock, editors, Formal Methods and Software Engineering: 5th International Conference on Formal Engineering Methods‚ ICFEM 2003: Singapore‚ November 5–7‚ 2003: Proceedings. Vol. 2885 of Lecture Notes in Computer Science. Pages 48–67. Springer−Verlag. 2003.

Details about An AMBA−ARM7 Formal Verification Platform | BibTeX data for An AMBA−ARM7 Formal Verification Platform | Download (pdf) of An AMBA−ARM7 Formal Verification Platform

Designing Correct Circuits (DCC'02)

Mary Sheeran and Tom Melham, editors

Proceedings of the Workshop on Designing Correct Circuits held during 6–7 April 2002 in Grenoble‚ France

Details about Designing Correct Circuits (DCC'02) | BibTeX data for Designing Correct Circuits (DCC'02)

PROSPER: An Investigation into Software Architecture for Embedded Proof Engines

Thomas F. Melham

In Alessandro Armando, editor, Frontiers of Combining Systems: 4th International Workshop‚ FroCoS 2002: Santa Margherita Ligure‚ Italy‚ April 8–10‚ 2002: Proceedings. Vol. 2309 of Lecture Notes in Artificial Intelligence. Pages 193–206. Springer−Verlag. 2002.

Details about PROSPER: An Investigation into Software Architecture for Embedded Proof Engines | BibTeX data for PROSPER: An Investigation into Software Architecture for Embedded Proof Engines | Download (pdf) of PROSPER: An Investigation into Software Architecture for Embedded Proof Engines

Abstraction by Symbolic Indexing Transformations

Thomas F. Melham and Robert B. Jones

In Mark D. Aagaard and John W. O'Leary, editors, Formal Methods in Computer−Aided Design: 4th International Conference‚ FMCAD 2002: Portland‚ OR‚ USA‚ November 6–8‚ 2002: Proceedings. Vol. 2517 of Lecture Notes in Computer Science. Pages 1–18. Springer−Verlag. 2002.

Details about Abstraction by Symbolic Indexing Transformations | BibTeX data for Abstraction by Symbolic Indexing Transformations | DOI (https://doi.org/10.1007/3-540-36126-X_1) | Download (pdf) of Abstraction by Symbolic Indexing Transformations

Formally Analyzed Dynamic Synthesis of Hardware

Kong Woei Susanto and Tom Melham

In The Journal of Supercomputing. Vol. 19. No. 1. Pages 7–22. May, 2001.

Details about Formally Analyzed Dynamic Synthesis of Hardware | BibTeX data for Formally Analyzed Dynamic Synthesis of Hardware | DOI (10.1023/A:1011132326153) | Link to Formally Analyzed Dynamic Synthesis of Hardware

Practical Formal Verification in Microprocessor Design

Robert B. Jones‚ John W. O'Leary‚ Carl−Johan H. Seger‚ Mark D. Aagaard and Thomas F. Melham

In IEEE Design & Test of Computers. Vol. 18. No. 4. Pages 16–25. 2001.

Details about Practical Formal Verification in Microprocessor Design | BibTeX data for Practical Formal Verification in Microprocessor Design | DOI (10.1109/54.936245) | Download (pdf) of Practical Formal Verification in Microprocessor Design

Correct Hardware Design and Verification Methods: 11th IFIP WG10.5 Advanced Research Working Conference‚ CHARME 2001: Livingston‚ Scotland‚ UK‚ September 4–7 2001: Proceedings

Tiziana Margaria and Tom Melham, editors

Details about Correct Hardware Design and Verification Methods: 11th IFIP WG10.5 Advanced Research Working Conference‚ CHARME 2001: Livingston‚ Scotland‚ UK‚ September 4–7 2001: Proceedings | BibTeX data for Correct Hardware Design and Verification Methods: 11th IFIP WG10.5 Advanced Research Working Conference‚ CHARME 2001: Livingston‚ Scotland‚ UK‚ September 4–7 2001: Proceedings | Link to Correct Hardware Design and Verification Methods: 11th IFIP WG10.5 Advanced Research Working Conference‚ CHARME 2001: Livingston‚ Scotland‚ UK‚ September 4–7 2001: Proceedings

An analysis of errors in interactive proof attempts

S. Aitken and T. Melham

In Interacting with Computers. Vol. 12. No. 6. Pages 565–586. June, 2000.

Details about An analysis of errors in interactive proof attempts | BibTeX data for An analysis of errors in interactive proof attempts

Xs are for Trajectory Evaluation‚ Booleans are for Theorem Proving (Extended Version)

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

No. TR−2000−52. Department of Computing Science‚ University of Glasgow. January, 2000.

Details about Xs are for Trajectory Evaluation‚ Booleans are for Theorem Proving (Extended Version) | BibTeX data for Xs are for Trajectory Evaluation‚ Booleans are for Theorem Proving (Extended Version) | Download (pdf) of Xs are for Trajectory Evaluation‚ Booleans are for Theorem Proving (Extended Version)

The PROSPER Toolkit

Louise A. Dennis‚ Graham Collins‚ Michael Norrish‚ Richard Boulton‚ Konrad Slind‚ Graham Robinson‚ Mike Gordon and Tom Melham

In Susanne Graf and Michael Schwartzbach, editors, 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: Berlin‚ Germany‚ March 25 – April 2‚ 2000: Proceedings. Vol. 1785 of Lecture Notes in Computer Science. Pages 78–92. Springer−Verlag. 2000.

Details about The PROSPER Toolkit | BibTeX data for The PROSPER Toolkit | Download (pdf) of The PROSPER Toolkit

A Methodology for Large−Scale Hardware Verification

Mark D. Aagaard‚ Robert B. Jones‚ Thomas F. Melham‚ John W. O'Leary and Carl−Johan H. Seger

In Jr. Warren A. Hunt and Steven D. Johnson, editors, Formal Methods in Computer−Aided Design: Third International Conference‚ FMCAD 2000: Austin‚ TX‚ USA‚ November 1–3‚ 2000: Proceedings. Vol. 1954 of Lecture Notes in Computer Science. Pages 263–282. Springer−Verlag. 2000.

Details about A Methodology for Large−Scale Hardware Verification | BibTeX data for A Methodology for Large−Scale Hardware Verification | Download (pdf) of A Methodology for Large−Scale Hardware Verification

Special Issue on Theorem Provers and Functional Programming

Tom Melham

In Journal of Functional Programming. Vol. 9. No. 2. Pages i−ii. March, 1999.

Details about Special Issue on Theorem Provers and Functional Programming | BibTeX data for Special Issue on Theorem Provers and Functional Programming

Xs Are for Trajectory Evaluation‚ Booleans Are for Theorem Proving

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

In Laurence Pierre and Thomas Kropf, editors, Correct Hardware Design and Verification Methods: 10th IFIP WG10.5 Advanced Research Working Conference‚ CHARME'99: Bad Herrenalb‚ Germany‚ September 27–29‚ 1999: Proceedings. Vol. 1703 of Lecture Notes in Computer Science. Pages 202–218. Springer−Verlag. 1999.

Details about Xs Are for Trajectory Evaluation‚ Booleans Are for Theorem Proving | BibTeX data for Xs Are for Trajectory Evaluation‚ Booleans Are for Theorem Proving | Download (pdf) of Xs Are for Trajectory Evaluation‚ Booleans Are for Theorem Proving

Interactive Theorem Proving: An Empirical Study of User Activity

J. S. Aitken‚ P. Gray‚ T. Melham and M. Thomas

In Journal of Symbolic Computation. Vol. 25. No. 2. Pages 263–284. February, 1998.

Details about Interactive Theorem Proving: An Empirical Study of User Activity | BibTeX data for Interactive Theorem Proving: An Empirical Study of User Activity

Formally Analysed Dynamic Synthesis of Hardware

Kong Woei Susanto and Tom Melham

In Jim Grundy and Malcolm Newey, editors, Theorem Proving in Higher Order Logics: Emerging Trends: 11th International Conference‚ TPHOLs'98‚ Canberra‚ September 27 – October 1‚ 1998: Supplementary Proceedings. Pages 105–117. Australian National University. 1998.

Details about Formally Analysed Dynamic Synthesis of Hardware | BibTeX data for Formally Analysed Dynamic Synthesis of Hardware

Dynamic Specialisation of XC6200 FPGAs by Partial Evaluation

Nicholas McKay‚ Tom Melham‚ Kong Woei Susanto and Satnam Singh

In Kenneth L. Pocek and Jeffrey M. Arnold, editors, Proceedings: IEEE Symposium on FPGAs for Custom Computing Machines: April 15–17‚ 1998‚ Napa Valley‚ California. Pages 308–309. IEEE Computer Society. 1998.

Details about Dynamic Specialisation of XC6200 FPGAs by Partial Evaluation | BibTeX data for Dynamic Specialisation of XC6200 FPGAs by Partial Evaluation | Download (pdf) of Dynamic Specialisation of XC6200 FPGAs by Partial Evaluation

ITP Project Anthology

Stuart Aitken‚ Philip Gray‚ Tom Melham and Muffy Thomas

No. TR−1997−36. Department of Computing Science‚ University of Glasgow. November, 1997.

Details about ITP Project Anthology | BibTeX data for ITP Project Anthology

Some Research Issues in Higher Order Logic Theorem Proving

Tom F. Melham

No. NS−96−7. Department of Computer Science‚ University of Aarhus. October, 1996.

Details about Some Research Issues in Higher Order Logic Theorem Proving | BibTeX data for Some Research Issues in Higher Order Logic Theorem Proving

Phases‚ Modes and Information Flow in Theory Development

J. S. Aitken‚ P. Gray‚ T. Melham and M. Thomas

In Nicholas A. Merriam, editor, User Interfaces for Theorem Provers: An International Workshop organised at the Department of Computer Science‚ University of York: 19th July 1996. Pages 1–8. University of York. 1996.

Details about Phases‚ Modes and Information Flow in Theory Development | BibTeX data for Phases‚ Modes and Information Flow in Theory Development

Five Axioms of Alpha−Conversion

Andrew D. Gordon and Tom Melham

In J. von Wright‚ J. Grundy and J. Harrison, editors, Theorem Proving in Higher Order Logics: 9th International Conference‚ TPHOLs'96: Turku‚ Finland‚ August 26–30‚ 1996: Proceedings. Vol. 1125 of Lecture Notes in Computer Science. Pages 173–190. Springer−Verlag. 1996.

Details about Five Axioms of Alpha−Conversion | BibTeX data for Five Axioms of Alpha−Conversion | Download (pdf) of Five Axioms of Alpha−Conversion

A Study Of User Activity In Interactive Theorem Proving

Stuart Aitken‚ Philip Gray‚ Tom Melham and Muffy Thomas

In Chris Johnson, editor, Task Centred Approaches To Interface Design: Glasgow Interactive Systems Group Research Review. Pages 195–218. Department of Computing Science‚ University of Glasgow. August, 1995.

GIST Technical Report G95.2

Details about A Study Of User Activity In Interactive Theorem Proving | BibTeX data for A Study Of User Activity In Interactive Theorem Proving

Interactive Proof Discovery: An Empirical Study of HOL Users

Stuart Aitken‚ Philip Gray‚ Tom Melham and Muffy Thomas

In Philip Gray, editor, User Interface Design for Theorem Proving Systems: An International Workshop organised by the ITP Project. Department of Computing Science‚ University of Glasgow. 1995.

Details about Interactive Proof Discovery: An Empirical Study of HOL Users | BibTeX data for Interactive Proof Discovery: An Empirical Study of HOL Users | Download (pdf) of Interactive Proof Discovery: An Empirical Study of HOL Users

Supplementary Proceedings of the 7th International Workshop on Higher Order Logic Theorem Proving and its Applications

Tom Melham and Juanito Camilleri, editors

Details about Supplementary Proceedings of the 7th International Workshop on Higher Order Logic Theorem Proving and its Applications | BibTeX data for Supplementary Proceedings of the 7th International Workshop on Higher Order Logic Theorem Proving and its Applications

The HOL Logic Extended with Quantification over Type Variables

Thomas F. Melham

In Formal Methods in System Design. Vol. 3. No. 1–2. Pages 7–24. 1994.

Details about The HOL Logic Extended with Quantification over Type Variables | BibTeX data for The HOL Logic Extended with Quantification over Type Variables | Download (pdf) of The HOL Logic Extended with Quantification over Type Variables

A Mechanized Theory of the Π−calculus in HOL

T. F. Melham

In Nordic Journal of Computing. Vol. 1. No. 1. Pages 50–76. 1994.

Details about A Mechanized Theory of the Π−calculus in HOL | BibTeX data for A Mechanized Theory of the Π−calculus in HOL

Higher Order Logic Theorem Proving and Its Applications: 7th International Workshop: Valletta‚ Malta‚ September 19–22‚ 1994: Proceedings

Thomas F. Melham and Juanito Camilleri, editors

Details about Higher Order Logic Theorem Proving and Its Applications: 7th International Workshop: Valletta‚ Malta‚ September 19–22‚ 1994: Proceedings | BibTeX data for Higher Order Logic Theorem Proving and Its Applications: 7th International Workshop: Valletta‚ Malta‚ September 19–22‚ 1994: Proceedings

Introduction to HOL: A theorem proving environment for higher order logic

M. J. C. Gordon and T. F. Melham, editors

Cambridge University Press. 1993.

Details about Introduction to HOL: A theorem proving environment for higher order logic | BibTeX data for Introduction to HOL: A theorem proving environment for higher order logic | Link to Introduction to HOL: A theorem proving environment for higher order logic

Higher Order Logic and Hardware Verification

T. Melham

Vol. 31 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press. 1993.

Details about Higher Order Logic and Hardware Verification | BibTeX data for Higher Order Logic and Hardware Verification | DOI (10.1017/CBO9780511569845) | Link to Higher Order Logic and Hardware Verification

Translating Dependent Type Theory into Higher Order Logic

Bart Jacobs and Tom Melham

In M. Bezem and J. F. Groote, editors, Typed Lambda Calculi and Applications: International Conference on Typed Lamda Calculi and Applications: TLCA '93: March‚ 16–18‚ 1993‚ Utrecht‚ The Netherlands: Proceedings. Vol. 664 of Lecture Notes in Computer Science. Pages 209–229. Springer−Verlag. 1993.

Details about Translating Dependent Type Theory into Higher Order Logic | BibTeX data for Translating Dependent Type Theory into Higher Order Logic

The HOL Logic Extended with Quantification over Type Variables

Thomas F. Melham

In Luc J. M. Claesen and Michael J. C. Gordon, editors, 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: Leuven‚ Belgium‚ 21–24 September 1992. Vol. 20 of IFIP Transactions A. Pages 3–17. North−Holland. 1993.

Details about The HOL Logic Extended with Quantification over Type Variables | BibTeX data for The HOL Logic Extended with Quantification over Type Variables

Reasoning with Inductively Defined Relations in the HOL Theorem Prover

Juanito Camilleri and Tom Melham

No. 265. Computer Laboratory‚ University of Cambridge. August, 1992.

Details about Reasoning with Inductively Defined Relations in the HOL Theorem Prover | BibTeX data for Reasoning with Inductively Defined Relations in the HOL Theorem Prover | Download (pdf) of Reasoning with Inductively Defined Relations in the HOL Theorem Prover

The HOL pred_sets Library

Computer Laboratory‚ University of Cambridge.

Computer Laboratory‚ University of Cambridge. February, 1992.

Details about The HOL pred_sets Library | BibTeX data for The HOL pred_sets Library

The HOL finite_sets Library

Computer Laboratory‚ University of Cambridge.

Computer Laboratory‚ University of Cambridge. February, 1992.

Details about The HOL finite_sets Library | BibTeX data for The HOL finite_sets Library

A Mechanized Theory of the π−calculus in HOL

T. F. Melham

No. 244. Computer Laboratory‚ University of Cambridge. January, 1992.

Details about A Mechanized Theory of the π−calculus in HOL | BibTeX data for A Mechanized Theory of the π−calculus in HOL

A Package for Inductive Relation Definitions in HOL

T. F. Melham

In Myla Archer‚ Jeffrey J. Joyce‚ Karl N. Levitt and Phillip J. Windley, editors, Proceedings of the 1991 International Workshop on the HOL Theorem Proving System and its Applications‚ Davis‚ California‚ August 28–30‚ 1991. Pages 350–357. IEEE Computer Society Press. 1992.

Details about A Package for Inductive Relation Definitions in HOL | BibTeX data for A Package for Inductive Relation Definitions in HOL | Download (pdf) of A Package for Inductive Relation Definitions in HOL

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

V. Stavridou‚ T. F. Melham and R. T. Boute, editors

Details about 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 | BibTeX data for 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

The HOL string Library

Computer Laboratory‚ University of Cambridge.

Computer Laboratory‚ University of Cambridge. June, 1991.

Details about The HOL string Library | BibTeX data for The HOL string Library

The HOL sets Library

Computer Laboratory‚ University of Cambridge.

Computer Laboratory‚ University of Cambridge. October, 1991.

Details about The HOL sets Library | BibTeX data for The HOL sets Library

A Mechanized Theory of the π−calculus in HOL

T. F. Melham

In G. Huet and G. Plotkin, editors, Proceedings of the Second Workshop on Logical Frameworks. Pages 219–237. University of Edinburgh. 1991.

Preliminary proceedings‚ published electronically after the workshop

Details about A Mechanized Theory of the π−calculus in HOL | BibTeX data for A Mechanized Theory of the π−calculus in HOL

Abstraction Mechanisms for Hardware Verification

Thomas F. Melham

In Michael Yoeli, editor, Formal Verification of Hardware Design. Pages 30–49. IEEE Computer Society Press. 1990.

Details about Abstraction Mechanisms for Hardware Verification | BibTeX data for Abstraction Mechanisms for Hardware Verification

Formalizing Abstraction Mechanisms for Hardware Verification in Higher Order Logic

Thomas Frederick Melham

PhD Thesis University of Cambridge. August, 1989.

Details about Formalizing Abstraction Mechanisms for Hardware Verification in Higher Order Logic | BibTeX data for Formalizing Abstraction Mechanisms for Hardware Verification in Higher Order Logic

Automating Recursive Type Definitions in Higher Order Logic

Thomas F. Melham

In G. Birtwistle and P. A. Subrahmanyam, editors, Current Trends in Hardware Verification and Automated Theorem Proving. Pages 341–386. Springer−Verlag. 1989.

Details about Automating Recursive Type Definitions in Higher Order Logic | BibTeX data for Automating Recursive Type Definitions in Higher Order Logic | Download (pdf) of Automating Recursive Type Definitions in Higher Order Logic

Automating Recursive Type Definitions in Higher Order Logic

Thomas F. Melham

No. 146. Computer Laboratory‚ University of Cambridge. September, 1988.

Details about Automating Recursive Type Definitions in Higher Order Logic | BibTeX data for Automating Recursive Type Definitions in Higher Order Logic

Using Recursive Types to Reason about Hardware in Higher Order Logic

Thomas F. Melham

No. 135. Computer Laboratory‚ University of Cambridge. May, 1988.

Details about Using Recursive Types to Reason about Hardware in Higher Order Logic | BibTeX data for Using Recursive Types to Reason about Hardware in Higher Order Logic

Hardware Verification by Formal Proof

Graham Birtwistle‚ Brian Graham‚ Tom Melham and Rick Schediwy

No. 88/328/40. Department of Computer Science‚ University of Calgary. October, 1988.

Details about Hardware Verification by Formal Proof | BibTeX data for Hardware Verification by Formal Proof

Hardware Verification by Formal Proof

G. Birtwistle‚ B. Graham‚ T. Melham and R. Schediwy

In V. K. Bhargava, editor, Proceedings of the Canadian Conference on Electrical and Computer Engineering‚ Vancouver‚ November 1988. Pages 379–384. Canadian Society for Electrical Engineering. 1988.

Details about Hardware Verification by Formal Proof | BibTeX data for Hardware Verification by Formal Proof

Using Recursive Types to Reason about Hardware in Higher Order Logic

Thomas F. Melham

In George J. Milne, editor, The Fusion of Hardware Design and Verification: Proceedings of the IFIP WG 10.2 Working Conference on The Fusion of Hardware Design and Verification: Glasgow‚ Scotland‚ 4–6 July‚ 1988. Pages 27–50. North−Holland. 1988.

Details about Using Recursive Types to Reason about Hardware in Higher Order Logic | BibTeX data for Using Recursive Types to Reason about Hardware in Higher Order Logic

Abstraction Mechanisms for Hardware Verification

Thomas F. Melham

In Graham Birtwistle and P. A. Subrahmanyam, editors, VLSI Specification‚ Verification and Synthesis. Vol. SECS35 of The Kluwer International Series in Engineeering and Computer Science. Pages 267–291. Kluwer Academic Publishers. 1988.

Details about Abstraction Mechanisms for Hardware Verification | BibTeX data for Abstraction Mechanisms for Hardware Verification

Abstraction Mechanisms for Hardware Verification

Thomas F. Melham

No. 106. Computer Laboratory‚ University of Cambridge. May, 1987.

Details about Abstraction Mechanisms for Hardware Verification | BibTeX data for Abstraction Mechanisms for Hardware Verification

Hardware Verification using Higher−Order Logic

Albert Camilleri‚ Mike Gordon and Tom Melham

In Dominique Borrione, editor, 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‚ Grenoble‚ France‚ 9–11 September‚ 1986. Pages 43–67. North−Holland. 1987.

Details about Hardware Verification using Higher−Order Logic | BibTeX data for Hardware Verification using Higher−Order Logic

Hardware Verification using Higher−Order Logic

Albert Camilleri‚ Mike Gordon and Tom Melham

No. 91. Computer Laboratory‚ University of Cambridge. June, 1986.

Details about Hardware Verification using Higher−Order Logic | BibTeX data for Hardware Verification using Higher−Order Logic

Specification and VLSI Design

Graham Birtwistle‚ Jeff Joyce‚ Breen Liblong‚ Tom Melham and Rick Schediwy

In George J. Milne and P. A. Subrahmanyam, editors, Formal Aspects of VLSI Design: Proceedings of the 1985 Edinburgh Workshop on VLSI: Edinburgh‚ Scotland‚ U.K.. Pages 83–97. North−Holland. 1986.

Details about Specification and VLSI Design | BibTeX data for Specification and VLSI Design

Towards a VLSI Design Tool System

Breen Liblong‚ Tom Melham‚ Graham Birtwistle and John Kendall

In INFOR: Information Systems and Operational Research. Vol. 23. No. 4. Pages 389–402. November, 1985.

Details about Towards a VLSI Design Tool System | BibTeX data for Towards a VLSI Design Tool System

Specification and VLSI Design

Graham Birtwistle‚ Jeff Joyce‚ Breen Liblong‚ Tom Melham and Rick Schediwy

No. 85/220/33. Department of Computer Science‚ University of Calgary. November, 1985.

Details about Specification and VLSI Design | BibTeX data for Specification and VLSI Design

EDICT: An Environment for Design Using Integrated Circuit Tools

Graham Birtwistle‚ David Hill‚ John Kendall‚ Bill Coates‚ Richard Esau‚ Wallace Kroeker‚ Breen Liblong‚ Erwin Liu‚ Tom Melham and Rick Schediwy

No. 84/155/13. Department of Computer Science‚ University of Calgary. June, 1984.

Details about EDICT: An Environment for Design Using Integrated Circuit Tools | BibTeX data for EDICT: An Environment for Design Using Integrated Circuit Tools

Towards a VLSI Design Tool System

Breen Liblong‚ Tom Melham‚ Graham Birtwistle and John Kendall

No. 84/175/33. Department of Computer Science‚ University of Calgary. November, 1984.

Details about Towards a VLSI Design Tool System | BibTeX data for Towards a VLSI Design Tool System

Exploiting Hierarchies in EDICT

B. Liblong‚ T. Melham and G. Birtwistle

In Proceedings of the 1984 Canadian Conference on VLSI. 1984.

Details about Exploiting Hierarchies in EDICT | BibTeX data for Exploiting Hierarchies in EDICT

Towards a VLSI Design Tool System

Breen Liblong‚ Tom Melham‚ Graham Birtwistle and John Kendall

In Leo Gotlieb, editor, Canadian Information Processing Society: SESSION 84: Proceedings. Pages 37–42. Canadian Information Processing Society. 1984.

Details about Towards a VLSI Design Tool System | BibTeX data for Towards a VLSI Design Tool System