Tom Melham : Publications
-
[1]
Contextualizing Formal Verification for Systems Security Engineering
Avi Shaked and Tom Melham
In IEEE Security & Privacy. Pages 2–11. 2024.
Details about Contextualizing Formal Verification for Systems Security Engineering | BibTeX data for Contextualizing Formal Verification for Systems Security Engineering | DOI (10.1109/MSEC.2024.3503753)
-
[2]
Modelling Tool Extension for Vulnerability Management
Avi Shaked‚ Nan Messe and Tom Melham
In MODELS 2024: ACM/IEEE 27th International Conference on Model Driven Engineering Languages and Systems: Companion Proceedings. Pages 56–60. Association for Computing Machinery. 2024.
Details about Modelling Tool Extension for Vulnerability Management | BibTeX data for Modelling Tool Extension for Vulnerability Management | DOI (10.1145/3652620.3687791)
-
[3]
Enhancing active model learning with equivalence checking using simulation relations
Natasha Yogananda Jeppu‚ Tom Melham and Daniel Kroening
In Formal Methods in System Design. Vol. 61. August, 2023.
Details about Enhancing active model learning with equivalence checking using simulation relations | BibTeX data for Enhancing active model learning with equivalence checking using simulation relations | DOI (10.1007/s10703-023-00433-y) | Download (pdf) of Enhancing active model learning with equivalence checking using simulation relations
-
[4]
A Formal CHERI−C Semantics for Verification
Seung Hoon Park‚ Rekha Pai and Tom Melham
In arXiv Computing Research Repository. Vol. arXiv:2211.07511 [cs.LO]. January, 2023.
Details about A Formal CHERI−C Semantics for Verification | BibTeX data for A Formal CHERI−C Semantics for Verification | Link to A Formal CHERI−C Semantics for Verification
-
[5]
A Formal CHERI−C Semantics for Verification
Seung Hoon Park‚ Rekha Pai and Tom Melham
In Sriram Sankaranarayanan and Natasha Sharygina, editors, Tools and Algorithms for the Construction and Analysis of Systems: TACAS 2023. Vol. 13993 of Lecture Notes in Computer Science. Pages 549–568. Springer‚ Cham. 2023.
Details about A Formal CHERI−C Semantics for Verification | BibTeX data for A Formal CHERI−C Semantics for Verification | DOI (10.1007/978-3-031-30823-9_28) | Download (pdf) of A Formal CHERI−C Semantics for Verification
-
[6]
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
-
[7]
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 and Fedor Shmarov
In IEEE Secure Development Conference‚ SecDev 2022‚ Atlanta‚ GA‚ USA‚ October 18–20‚ 2022. Pages 52–58. IEEE. 2022.
Details about Position Paper: Towards a Hybrid Approach to Protect Against Memory Safety Vulnerabilities | BibTeX data for Position Paper: Towards a Hybrid Approach to Protect Against Memory Safety Vulnerabilities | DOI (10.1109/SecDev53368.2022.00020)
-
[8]
Exposing Previously Undetectable Faults in Deep Neural Networks
Isaac Dunn‚ Hadrien Pouget‚ Daniel Kroening and Tom Melham
In arXiv Computing Research Repository. Vol. arXiv:2106.00576 [cs.LG]. June, 2021.
Details about Exposing Previously Undetectable Faults in Deep Neural Networks | BibTeX data for Exposing Previously Undetectable Faults in Deep Neural Networks | Link to Exposing Previously Undetectable Faults in Deep Neural Networks
-
[9]
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. Association for Computing Machinery. 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) | Download (pdf) of Exposing Previously Undetectable Faults in Deep Neural Networks
-
[10]
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]
-
[11]
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
-
[12]
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
-
[13]
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
-
[14]
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
-
[15]
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
-
[16]
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
-
[17]
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
-
[18]
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
-
[19]
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
-
[20]
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)
-
[21]
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
-
[22]
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
-
[23]
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
-
[24]
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
-
[25]
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
-
[26]
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
-
[27]
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
-
[28]
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)
-
[29]
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
-
[30]
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
-
[31]
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
-
[32]
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
-
[33]
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
-
[34]
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
-
[35]
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)
-
[36]
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
-
[37]
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
-
[38]
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)
-
[39]
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)
-
[40]
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
-
[41]
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
-
[42]
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)
-
[43]
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)
-
[44]
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
-
[45]
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
-
[46]
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
-
[47]
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
-
[48]
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
-
[49]
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
-
[50]
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
-
[51]
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
-
[52]
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
-
[53]
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
-
[54]
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
-
[55]
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
-
[56]
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
-
[57]
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
-
[58]
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
-
[59]
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
-
[60]
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
-
[61]
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
-
[62]
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
-
[63]
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
-
[64]
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
-
[65]
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
-
[66]
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
-
[67]
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)
-
[68]
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
-
[69]
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
-
[70]
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
-
[71]
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
-
[72]
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
-
[73]
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
-
[74]
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)
-
[75]
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
-
[76]
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
-
[77]
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
-
[78]
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
-
[79]
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
-
[80]
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
-
[81]
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
-
[82]
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
-
[83]
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
-
[84]
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
-
[85]
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
-
[86]
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
-
[87]
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
-
[88]
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
-
[89]
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
-
[90]
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
-
[91]
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
-
[92]
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
-
[93]
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
-
[94]
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
-
[95]
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
-
[96]
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
-
[97]
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
-
[98]
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
-
[99]
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
-
[100]
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
-
[101]
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
-
[102]
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
-
[103]
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
-
[104]
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
-
[105]
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
-
[106]
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
-
[107]
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
-
[108]
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
-
[109]
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
-
[110]
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
-
[111]
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
-
[112]
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
-
[113]
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
-
[114]
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
-
[115]
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
-
[116]
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
-
[117]
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
-
[118]
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
-
[119]
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
-
[120]
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
-
[121]
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
-
[122]
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
-
[123]
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
-
[124]
-
[125]
-
[126]