Publications
2023
Dimosthenis Masouros, Dimitrios Soudris, Georgios Gardikis, Victoria Katsarou, Maria Christopoulou, George Xilouris, Hugo Ramón, Antonio Pastor Fabrizio Scaglione, Cristian Petrollini, António Pinto, João P. Vilela, Antonia Karamatskou, Nikolaos Papadakis, Anna Angelogianni, Thanassis Giannetsos, Luis Javier García Villalba, Jesús A. Alonso-López, Martin Strand, Gudmund Grov, Anastasios N. Bikos, Kostas Ramantas, Ricardo Santos, Fábio Silva, and Nikolaos Tsampieris. Towards privacy-first security enablers for 6G networks: the PRIVATEER approach, In Embedded Computer Systems: Architectures, Modeling, and Simulation. SAMOS 2023. Lecture Notes in Computer Science, vol 14385. Springer, Cham, pp 379–391, https://doi.org/10.1007/978-3-031-46077-7_25 [link]
2022
Håkon Svee Eriksson and Gudmund Grov. Towards XAI in the SOC - a user centric study of explainable alerts with SHAP and LIME. 2022 IEEE International Conference on Big Data (Big Data), Osaka, Japan, 2022, pp. 2595-2600, doi: 10.1109/BigData55660.2022.10020248. [link]
Julie Gjerstad, Fikret Kadiric, Gudmund Grov, Espen Hammer Kjellstadli and Markus Leira Asprusten. LADEMU: a modular & continuous approach for generating labelled APT datasets from emulations. 2022 IEEE International Conference on Big Data (Big Data), Osaka, Japan, 2022, pp. 2610-2619, doi: 10.1109/BigData55660.2022.10020549. [link]
Andreas Dybvik Kaasen, Gudmund Grov, Federico Mancini and Magnus Baksaas. Towards Data-Driven Autonomous Cyber Defence for Military Unmanned Vehicles With Autonomous Capabilities - Threats & Attacks. MILCOM 2022 - 2022 IEEE Military Communications Conference (MILCOM), Rockville, MD, USA, 2022, pp. 861-866, doi: 10.1109/MILCOM55135.2022.10017692. [link]
2021
Markus Asprusten, Julie Gjerstad, Gudmund Grov, Espen Kjellstadli, Robert Flood, Henry Clausen and David Aspinall. A containerised approach to labelled C&C traffic. In No. 3 (2021): NISK Norsk informasjonssikkerhetskonferanse [link]
Gudmund Grov, Andrew Ireland and and Teresa Llano. Reasoned Modelling: Harnessing the Synergies Between Reasoning and Modelling. In Mathematical Reasoning: The History and Impact of the DReaM Group, pages 105-127, Springer, Cham. https://doi.org/10.1007/978-3-030-77879-8_6, 2021.
Henry Clausen, Gudmund Grov and David Aspinall. CBAM: A Contextual Model for Network Anomaly Detection. Computers 2021, 10(6):79. https://doi.org/10.3390/computers10060079
2020
Henry Clausen, Gudmund Grov, Marc Sabate and David Aspinall. Better anomaly detection for access attacks using deep bidirectional LSTMs. In Proceedings of 3rd International Conference on Machine Learning for Networking (MLN 2020), LNCS, volume 12629, pages 1-18, 2021.
2019
Gudmund Grov, Federico Mancini and Elsie Margrethe Staff Mestl. Challenges for Risk and Security Modelling in Enterprise Architecture. In Proceedings of the12th IFIP Working Conference on the Practice of Enterprise Modeling PoEM 2019), Lecture Notes in Business Information Processing (LNBIP), volume 369, pages 215-225, 2019 [link]
Gudmund Grov, Marc Sabate, Wei Chen and David Aspinall. Towards Intelligible Robust Anomaly Detection by Learning Interpretable Behavioural Models. In Proceedings of the 12th Norwegian Information Security Conference (NISK 2019), Volume 12 of the NISK Journal [link]
Yuhui Lin, Alan Bundy, Gudmund Grov and Ewen Maclean. Automating Event-B invariant proofs by rippling and proof patching. In Formal Aspects of Computing, Volume 31, Issue 1, pages 95-129, 2019.
2017
Gudmund Grov and Andrew Ireland (editors). Science of Computer Programming Special issue on Automated Verification of Critical Systems (AVoCS 2015). Volume 148, Pages 1-212 (15 November 2017).
Gudmund Grov, Duncan Cameron and Leon McGregor. DAReing to reduce the annotation overheads of verified programs. In arXiv:1706.04023 [link]
Gudmund Grov and Yuhui Lin. The Tinker tool for graphical tactic development. In Software Tools for Technology Transfer, pages 1-17, DOI: 10.1007/s10009-017-0452-7, 2017 [link].
Gudmund Grov, Mohammad Hamdan, Smitha S. Kumar, Manuel Maarek, Léon McGregor, Talal A. G. Shaikh, J. B. Wells, and Hind Zantout. Transition from passive learner to critical evaluator through peer-testing of programming artifacts. In STEM HE, Edinburgh, UK, 2017.
Gudmund Grov, Mohammad Hamdan, Smitha S. Kumar, Manuel Maarek, Léon McGregor, Talal A. G. Shaikh, J. B. Wells, and Hind Zantout. Transition from Passive Learner to Critical Evaluator through Peer-Testing of Programming Artefacts. New Directions in the Teaching of Physical Sciences, 12, November 2017 [link].
2016
Yuhui Lin, Gudmund Grov and Rob Arthan. Understanding and maintaining tactics graphically OR how we are learning that a diagram can be worth more than 10K LoC. In Journal of Formalized Reasoning, Volume 9, No 2 (2016), pages 69-130 [link].
Gudmund Grov, Yuhui Lin and Pierre Le Bras.The Tinker GUI for graphical proof strategies (tool demo). In Proceedings of 3rd Workshop on Formal Integrated Development Environment, Volume 240, pages 98-101. EPTCS, 2016 [link].
Gudmund Grov, Yuhui Lin, Leon McGregoer, Vytautas Tumas and Duncan Cameron. Extending the Dafny IDE with tactics and dead annotation analysis (tool demo). In Proceedings of 3rd Workshop on Formal Integrated Development Environment, Volume 240, pages 102-104. EPTCS, 2016 [link].
Rajiv Murali, Andrew Ireland and Gudmund Grov. A Formal Approach to Use Case Driven Testing. In Proceeding of Workshop on Formal and Model-Driven Techniques for Developing Trustworthy Systems 2016. To appear as a technical report of Newcastle University and in ACM Computing Research Repository (CORR).
Duncan Cameron, Gudmund Grov and Leon McGregor. What is your actual annotation overhead? In informal proceedings of 28th Nordic Workshop on Programming Theory, 2016. [link]
Gudmund Grov, Yuhui Lin and Vytautas Tumas. Mechanised Verification Patterns for Dafny. In the 21st International Conference on Formal Methods (FM 2016), volume 9995 of LNCS, pages 326-343, Springer, 2016.
Gudmund Grov, Verena Rieser, Michael Lones and Graeme Reid. Transition of automated feedback and marking into student’s learning environment. QAA Enhancement report (phase 2), 2016. [ link ]
Daniel Raggi, Alan Bundy, Gudmund Grov and Alison Pease. Automating change of representation for proofs in discrete mathematics (extended version). Journal of Mathematics in Computer Science, doi:10.1007/s11786-016-0275-z
Gudmund Grov, Andrew Ireland, Teresa Llano, Peter Kovacs, Simon Colton and Jeremy Gow. Semi-Automated Design Space Exploration for Formal Modelling. In the 5th International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z (ABZ 2016), volume 9675 of LNCS, pages 282–289, Springer, 2016. [Long version on ArXiV].
Yuhui Lin, Gudmund Grov, Colin O'Halloran and Priiya G. A super industrial application of PSGraph. In the 5th International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z (ABZ 2016), volume 9675 of LNCS, pages 319–325, Springer, 2016.
Yibo Liang, Yuhui Lin and Gudmund Grov. ‘The Tinker’ for Rodin. In the 5th International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z (ABZ 2016), volume 9675 of LNCS, pages 262–268, Springer, 2016.
Rajiv Murali, Andrew Ireland and Gudmund Grov. UC-B: Use Case Modelling with Event-B. In the 5th International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z (ABZ 2016), volume 9675 of LNCS, pages 297–302, Springer, 2016.
Gudmund Grov and Vytautas Tumas. Tactics for the Dafny Program Verifier. In the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2016), volume 9636 of LNCS, pages 36–53, Springer, 2016. (Nominated for EASST award)
Yuhui Lin, Pierre Le Bras and Gudmund Grov. Developing & Debugging Proof Strategies by Tinkering. In the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2016), volume 9636 of LNCS, pages 573–579, Springer, 2016.
2015
Gudmund Grov and Andrew Ireland (editors). Proceedings of the 15th International Workshop on Automated Verification of Critical Systems. Volume 72 of the Electronic Communications of the EASST Open Access Journal [link]
Gudmund Grov and Andrew Ireland (editors). Pre-proceedings of the 15th International Workshop on Automated Verification of Critical Systems. Department of Computer Science, Heriot-Watt University. MACS CS Technical Report HW-MACS-TR-0109 [PDF].
Andrius Velykis, Gudmund Grov and Leo Freitas (editors). Contribution of the AI4FM 2015 Workshop, Edinburgh, 2015. Department of Computing Science, Newcastle University. Technical report (to appear) [PDF].
Colin Farquhar, Gudmund Grov, Andrew Cropper, Stephen Muggleton and Alan Bundy. Typed meta-interpretive learning for proof strategies. In AI4FM 2015 (extended abstract) [link]
Pierre Le Bras, Yuhui Lin and Gudmund Grov. Tinker: A Graph Based Proof Strategy System. In AI4FM 2015 (extended abstract) [link]
Gudmund Grov, Graeme Reid and Verena Rieser. Helping 1st Year CS Students to Become Independent Learner Through Automated Feedback. QAA Enhancement report, 2015. [ link ]
Colin Farquhar, Gudmund Grov, Andrew Cropper, Stephen Muggleton and Alan Bundy. Typed meta-interpretive learning for proof strategies. Short paper in the 25th International Conference on Inductive Logic Programming (ILP 2015). [link, PDF]
Daniel Raggi, Alan Bundy, Gudmund Grov and Alison Pease. Automating change of representation for proofs in discrete mathematics. In Conference of Intelligent Computer Mathematics (CICM 2015), volume 9150 of LNCS, pages 227–242, Springer, 2015. [ArXiV]
Rajiv Murali, Andrew Ireland and Gudmund Grov. A Rigorous Approach to Combining Use Case Modelling and Accident Scenarios. In the 7th NASA Formal Methods Symposium (NFM 2015), volume 9058 of LNCS, pages 263–278, Springer, 2015.
2014
Gudmund Grov. Some ideas for Program Verifier Tactics. In ArXiv:1406.2824.
Gudmund Grov and Thomas Wies (editors). Science of Computer Programming Special Issue on Invariant Generation. Volume 93, Part B. Pages 87-182 (1 November 2014). DOI: 10.10.1016/j.scico.2014.05.010
Gudmund Grov, Aleks Kissinger and Yuhui Lin. Tinker, Tailor, Solver, Proof. In Proceedings of Eleventh Workshop on User Interfaces for Theorem Provers (UITP 2014), Vienna, Austria, 2014. Volume 167 of Electronic Proceedings of Theoretical Computer Science, pages. 23-34. [webpage]
Hans-Wolfgang Loidl and Gudmund Grov. Reasoning about Resources in the Embedded Systems Language Hume. In Third International Workshop on Foundational and Practical Aspects of Resource Analysis, volume 8552 of LNCS, pages 110–126, Springer, 2014. [webpage]
Gudmund Grov. Continous assessment of first year programming courses. Lightning talk given the ICER 2014 conference [webpage]
Gudmund Grov, Colin Farquhar, Alison Pease and Simon Colton. Tinkering by Theory Formation, In AI4FM 2014 , Singapore, 2014. Department of Computer Science, Heriot-Watt University. Technical report HW-MACS-TR-0100.
Gudmund Grov, Leo Freitas and Iain Whiteside, editors. Contribution of the AI4FM 2014 Workshop, Singapore, 2014. Department of Computer Science, Heriot-Watt University. Technical report HW-MACS-TR-0100.
Ewen Maclean, Andrew Ireland and Gudmund Grov. Proof Automation for Functional Correctness in Separation Logic. In Journal of Logic and Computation Special Issue for Roy Dyckhoff, volume 26, issue 2, pages 641-675. DOI: 0.1093/logcom/exu032. [webpage]
2013
Gudmund Grov, Aleks Kissinger and Yuhui Lin. A Graphical Language for Proof Strategies. In Logic for Programming Artificial Intelligence and Reasoning (LPAR-19), volume 8312 of LNCS, pages 324–339, Springer, 2013.
Gudmund Grov and Ewen Maclean. Towards Automated Proof Strategy Generalisation. In arXiv:1303.2975
Gudmund Grov, Ewen Maclean, and Leo Freitas, editors. Contributions to AI4FM 2013, Rennes, France, 2013. Department of Computer Science, Heriot-Watt University. Technical report HW-MACS-TR-0100.
Gudmund Grov, Aleks Kissinger, Yuhui Lin, Ewen Maclean and Colin Farquhar. Drawing Proof Strategies. In AI4FM 2013, Rennes, France, 2013. Department of Computer Science, Heriot-Watt University. Technical report HW-MACS-TR-0100.
E.Komendantskaya, J.Heras and G.Grov. Machine-Learning for Proof General: interfacing interfaces. In Proceedings 10th International Workshop On
User Interfaces for Theorem Provers, volume 118 of Electronic Proceedings of Theoretical Computer Science, pages. 15-41. [webpage]
Colin Farquhar and Gudmund Grov. Structured Proofs from a Graphical Proof Strategy Language. In the 20th Automated Reasoning Workshop (ARW 2013), Dundee, 11-12 April, 2013.
2012
Gudmund Grov, Andrew Ireland, and Maria Teresa Llano. Refinement plans for informed formal design. In John Derrick, John A. Fitzgerald, Stefania Gnesi, Sarfraz Khurshid, Michael Leuschel, Steve Reeves, and Elvinia Riccobene, editors, Abstract State Machines, Alloy, B, VDM, and Z - Third International Conference, ABZ 2012, volume 7316 of LNCS, pages 208–222. Springer, 2012.
I. Whiteside, D. Aspinall and G. Grov. An Essence of SSReflect. In CICM’12. Iain Whiteside, David Aspinall, and Gudmund Grov. An essence of SSReflect. In Johan Jeuring, John A. Campbell, Jacques Carette, Gabriel Dos Reis, Petr Sojka, Makarius Wenzel, and Volker Sorge, editors, Conferences on Intelligent Computer Mathematics (CICM 2012), volume 7362 of LNCS, pages 186–201. Springer, 2012.
Gudmund Grov, Ekaterina Komendantskaya, and Alan Bundy. A statistical relational learning challenge – extracting proof strategies from exemplar proofs. In ICML-12 Workshop on Statistical Relational Learning (SRL 2012), Edinburgh, Scotland, June 2012.
Yuhui Lin, Alan Bundy, and Gudmund Grov. The use of Rippling to automate Event-B invariant preservation proofs. In Alwyn Goodloe and Suzette Person, editors, In 4th International NASA Formal Methods Symposium (NFM 2012), volume 7226 of LNCS, pages 231–236. Springer, 2012.
Yuhui Lin, Alan Bundy, and Gudmund Grov. The use of Rippling to automate Event-B invariant preservation proofs. In IJCAR Workshop on Automated Theory eXploration (ATX 2012), Manchester, UK, June 2012.
2011
G. Grov and G. Michaelson. Hume box calculus: robust system development through software transformation. In Higher-Order and Symbolic Computation, Volume 23, Issue 2, pp 191–226, Springer, 2011.
A. Ireland, G. Grov, M.T. Llano and M. Butler. Reasoned Modelling Critics: Turning Failed Proofs into Modelling Guidance. In Science of Computer Programming : Abstract State Machines, Alloy, B and Z - Selected Papers from ABZ, volume 78, Issue 3, pages 293–309, Elsevier, 2011.
G. Michaelson and G. Grov. Reasoning about multi-process systems with the box calculus. In Central European Functional Programming School 2011, volume 7241 of LNCS, pages 279-33, Springer, 2011.
E. Maclean, A. Ireland and G. Grov. The CORE System: Animation and Functional Correctness of Pointer Programs. In 26th IEEE/ACM International Conference on Automated Software Engineering (ASE 2011), pages 588 - 591, ACM Press.
I. Whiteside, D. Aspinall, L. Dixon and G. Grov. Towards Formal Proof Script Refactoring. In J. Davenport, W. Farmer. J. Urban and F. Rabe (Eds) Conference of Intelligent Computer Mathematics (CICM 2011),Volume 6824 of LNCS, pages 260-275, Spring 2011 (best paper).
G. Grov and S. Merz. A Definitional Encoding of TLA* in Isabelle/HOL. In the Archive of Formal Proofs, 2011 [link]
A. Bundy, G. Grov and Y. Lin. Productive use of failure in top-down formal methods. In Proceedings of 18th Automated Reasoning Workshop, University of Glasgow, Department of Computer Science, Technical Report TR-2011-327, A. Miller & R. Kirwan (Eds), 2011, pp. 13-14.
2010
A. Pease, A. Smaill, S. Colton, A. Ireland, M.T. Llano, R. Ramezani, G. Grov and M. Guhe. Applying Lakatos-style reasoning to AI problems. In Thinking Machines and the Philosophy of Computer Science: Concepts and Principles. J. Vallverdu (Ed), IGI Global, PA, USA, 2010, Chapter 10, pp. 149-173.
A. Ireland, G. Grov and M. Butler. Reasoned Modelling Critics: Turning Failed Proofs into Modelling Guidance. In M. Frappier, U. Glasser, S. Khurshid, R. Laleau and S. Reeves (Eds) Proceedings of ABZ 2010, Voume 5977 of LNCS, pages. 189-202, Springer, 2010,
G. Grov and C. B. Jones. AI4FM — A new project seeking challenges! In Proceedings of Tools & Experiments workshop at VSTTE 2010.
E. Maclean, A. Ireland, G. Grov. Functional Correctness for Pointer Programs. In Proceedings of Tools & Experiments workshop at VSTTE 2010.
E. Maclean, A. Ireland and G. Grov. Synthesising Functional Invariants in Separation Logic. In N. Bjorner, A. Voronkov and L. Kovacs (Eds) the third International Workshop on Invariant Generation (WING 2010), with FLoC. Volume 1 of the EPiC series (EasyChair Proceedings of Computing), pages 183-184, 2010.
C. B. Jones, G. Grov and A. Bundy. Ideas for a high-level proof strategy language. In Proceedings of 5th International Workshop of Automated Formal Methods, 2010, B. Dutertre and H. Saidi (Eds).
M.T. Llano, G. Grov and A. Ireland. Automatic Guidance for Refinement Based Formal Methods. In Proceedings of 5th International Workshop of Automated Formal Methods, 2010, B. Dutertre and H. Saidi (Eds).
G. Grov, A. Bundy, C. B. Jones and A. Ireland. The AI4FM approach for proof automation within formal methods — A Grand Challenge 6 "Dependable Systems Evolution" project. In UKCRC Submissions to Grand Challenges in Computing Research 2010.
G. Grov, A. Bundy and L. Dixon. A small experiment in Event-B rippling. In Proceedings of AVoCS 2010 and Rodin User and Developer Workshop 2010.
M.T. Llano, A. Ireland and G. Grov. Refinement plans for reasoned modelling. In Proceedings of AVoCS 2010 and Rodin User and Developer Workshop 2010.
A. Bundy, G. Grov and C.B. Jones. An outline of a proposed system that learns from experts how to discharge proof obligations automatically. In Refinement Based Methods for the Construction of Dependable Systems: 09381 Extended Abstracts Collection. Editors J-R. Abrial, M. Butler, R. Joshi, E. Troubitsyna, J.C.P. Woodcock. Dagstuhl Seminar Proceedings, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2010.
A. Ireland and G. Grov. Reasoned Modelling: Combining Proof and Modelling Patterns to Guide Systems Design. In Refinement Based Methods for the Construction of Dependable Systems: 09381 Extended Abstracts Collection. Editors J-R. Abrial, M. Butler, R. Joshi, E. Troubitsyna, J.C.P. Woodcock. Dagstuhl Seminar Proceedings, Schloss Dagstuhl - Leibniz- Zentrum fuer Informatik, 2010.
2009
G. Grov, G. Michaelson, C. Herrmann, H.W. Loidl, S. Jost and K. Hammond. Hume Cost Analysis for Imperative Programs. In Proceedings of International Conference on Software Engineering Theory and Practice 2009.
A. Bundy, G. Grov, and C. B. Jones. Learning from experts to aid the automation of proof search. In PreProceedings of the Ninth International Workshop on Automated Verification of Critical Systems, Swansea University Computer Science Technical Report CSR-2-2009, L. O'Reilly and M. Roggenbach (Eds) 2009, pp. 229-232
G. Grov and A. Ireland. Towards Automated Property Discovery within Hume. In 2nd International Workshop on Invariant Generation (WING'09), a satellite workshop of ETAPS-09, York, UK, 2009. Volume 1 of the EPiC series (EasyChair Proceedings of Computing), pages 111-127, 2010.
G. Grov, Reasoning About Correctness Properties of a Coordination Language, PhD thesis, Heriot-Watt University, March 2009. [link, PDF]
G. Grov, A. Ireland, M. Butler, A. Bundy and C. Jones. A Proposal for a Rodin Proof Planner & Reasoned Modelling Plug-in. In Proceedings of Rodin User and Developer Workshop 2009.
G. Michaelson, G. Grov and A. Al Zain. Multi-core parallelisation of Hume through structured transformation. In Draft Proceedings of 21st International Symposium on Implementation and Application of Functional Languages, 2009.
G. Grov, G. Michaelson, H-W. Loidl, C. Herrmann, S. Jost and K. Hammond. An application of Hume analysis to imperative programs. In Draft Proceedings of 10th Symposium on Trends in Functional Programming, 2009. Z. Horvath and V. Zsok (Eds), pages 27-42.
2008
G. Grov, R. Pointon, G. Michaelson and A. Ireland. Preserving Coordination Properties when Transforming Concurrent System Components. In Proceedings of 23rd Annual ACM Symposium on Applied Computing (SAC’08), ACM Press, 2008, pp. 126-127.
2007
G. Grov and G. Michaelson. Towards a Box Calculus for Hierarchical Hume. In Trends in Functional Programming, M. Morazan and H. Nilsson (Eds),Volume 8, Intellect, 2007, Chapter 5, pp 71-88.
K. Hammond, G. Grov, G. Michaelson and A. Ireland. Low-Level Programming in Hume: an Exploration of the HW-Hume Level. In Proceedings of 18th International Symposium on Implementation and Application of Functional Languages (IFL’06), Z. Horvath, V. Zsok and A. Butterfield (Eds), volume 4449 of LNCS, Springer 2007.
G. Grov, G. Michaelson and A. Ireland. Formal Verification of Concurrent Scheduling Strategies using TLA. In Proceedings of the International Conference on Parallel and Distributed Systems (3rd IEEE Workshop on Scheduling and Resource Management for Parallel and Distributed Systems), R. Kettimuthu (Eds), pages 1-6, IEEE, 2007,
G. Grov. Verified Transformations Guided by Static Analysis: The Hume Approach Towards Correct Software with Bounds on Time & Space. Abstract for poster session at Quest 2007.
2006
G. Michaelson, R. Pointon, G. Grov and A. Ireland. Recursion, Iteration and Hume Scheduling. In Draft Proceedings of 7th Symposium on Trends in Functional Programming, H. Nilsson and M van Eekling (Eds), 2006, pages 403-416.
K. Hammond, G. Michaelson and G. Grov. Towards Hardware/Software Codesign: Exploring the HW-Hume Level. In Z. Horvath and V. Zsok (Eds), In Draft Proceedings 18th International Symposium on Implementation and Application of Functional Programs, 2006. pp 99-114.
2005
G. Grov. Verifying the Correctness of Hume Programs: An Approach Combining Deductive and Algorithmic Reasoning. In Proceedings of 20th IEEE/ACM International Conference on Automated Software Engineering, ACM Press, pages 444-447, 2005.
2004
G. Grov, A. Ireland and G. Michaelson. Model Checking HW-Hume. In Draft Proceedings of 5th International Symposium on Trends in Functional Programming, H.W. Loidl (Eds), 2004, pp. 33-48.
G. Grov, Model Checking HW-Hume, MSc thesis, Heriot-Watt University, 2004.