Research interests
I work in the Dependable Systems Group at Heriot-Watt University, and closely with the Mathematical Reasoning (Dream) Group / CISA / School of Informatics / University of Edinburgh - as well as CSR / Newcastle University. My main research interest is in the are of formal methods, automated reasoning and artificial intelligence. In particular, the use of artificial intelligence and automated reasoning in modelling and proof within formal methods. 

I am involved in the following projects:
AI4FM The goal of the AI4FM project is to use AI to automate proofs within formal methods. See project webpage for more details about the project, the people involved, papers and talks.
Reasoned modelling combines proof and reasoning patterns to guide both proof but also modelling within formal methods. I’ve been involved developing this technique mainly with Andrew Ireland, Teresa Llano and Michael Butler.
Functional verification in separation logic. I am involved with the CORE project, where I work worked with Andrew Ireland and Ewen Maclean on functional verification of properties in separation logic.
Hume. My PhD work was concerned with functional correctness of Hume programs using Lamport’s TLA logic and Isabelle/HOL. I have been employed on the EU-funded EmBounded project, where I addressed model checking of Hume, and resource verification of imperative programs using Hume. My main contribution is the development of the Hume box calculus, joint with G. Michaelson.

Selected papers [bibtex]
This bibtex file contains all my papers. Below I highlight my favourite paper from each of the above research projects:
A. Ireland, G. Grov, M.T. Llano and M. Butler. Reasoned Modelling Critics: Turning Failed Proofs into Modelling Guidance. To appear in Science of Computer Programming, 2011.
Introduces the reasoned modelling ideas and gives a thorough description of the reasoned modelling critics.
G. Grov and G. Michaelson. Hume box calculus: robust system development through software transformation. In Higher-Order and Symbolic Computation, 2011, Springer, pp 1-36. [link] 
Introduces the Hume box calculus, including examples of use.
A. Bundy, G. Grov, and C. B. Jones. Learning from experts to aid the automation of proof search. Short contribution to AVoCS’09. [proceeding]
Summarises the ideas behind the AI4FM project.
E. Maclean, A. Ireland and G. Grov. The CORE System: Animation and Functional Correctness of Pointer Programs. To appear as Tool paper in IEEE/ACM International Conference on Automated Software Engineering, 2011
Describes the CORE system for functional verification in separation logic.

PhD Supervision
I am involved in the supervision of the following  PhD students:
Maria Teresa Llano Rodriguez (Heriot-Watt)
Iain Whiteside (Edinburgh)
Yuhui Lin (Edinburgh)
Daniel Raggi (Edinburgh)
Colin Farquhar (Heriot-Watt)

Teaching
Reasoning, Modelling & Refinement in Event-B. Guest lecture given at Automated Reasoning module at School of Informatics, University of Edinburgh (November’09) [slides-4up | case-study | Rodin files]


Last updated: 1 October 2012http://www.macs.hw.ac.uk/~dsghttp://www.hw.ac.uk/http://dream.inf.ed.ac.uk/http://dream.inf.ed.ac.uk/http://www.cisa.inf.ed.ac.uk/http://www.ed.ac.uk/schools-departments/informatics/http://www.ed.ac.uk/http://www.csr.ncl.ac.uk/http://www.ncl.ac.uk/http://www.ncl.ac.uk/http://www.ai4fm.orghttp://www.ai4fm.org/http://www.ai4fm.org/http://www.ai4fm.org/http://www.macs.hw.ac.uk/~air/http://www.macs.hw.ac.uk/~mtl4/http://users.ecs.soton.ac.uk/mjb/http://www.macs.hw.ac.uk/core/http://www.macs.hw.ac.uk/core/http://www.macs.hw.ac.uk/~air/http://www.macs.hw.ac.uk/~eahm2/http://www.macs.hw.ac.uk/~greg/hume/http://www.hume-lang.orghttp://www.embounded.orghttp://www.macs.hw.ac.uk/~greg/Gudmunds_homepage_files/gudmund-papers.bibGudmunds_homepage_files/gudmund-papers_1.bibhttp://www.springerlink.com/content/x02086ql64405p80/http://www.cs.swan.ac.uk/avocs09/PreProceedings.pdfhttp://www.macs.hw.ac.uk/~mtl4/http://homepages.inf.ed.ac.uk/s0569509/http://homepages.inf.ed.ac.uk/s1064212/Gudmunds_homepage_files/AR-lecture17-4sided.pdfGudmunds_homepage_files/plc-EventB-2sided.pdfGudmunds_homepage_files/Rodin-power-lock-controller.zipshapeimage_1_link_0shapeimage_1_link_1shapeimage_1_link_2shapeimage_1_link_3shapeimage_1_link_4shapeimage_1_link_5shapeimage_1_link_6shapeimage_1_link_7shapeimage_1_link_8shapeimage_1_link_9shapeimage_1_link_10shapeimage_1_link_11shapeimage_1_link_12shapeimage_1_link_13shapeimage_1_link_14shapeimage_1_link_15shapeimage_1_link_16shapeimage_1_link_17shapeimage_1_link_18shapeimage_1_link_19shapeimage_1_link_20shapeimage_1_link_21shapeimage_1_link_22shapeimage_1_link_23shapeimage_1_link_24shapeimage_1_link_25shapeimage_1_link_26shapeimage_1_link_27shapeimage_1_link_28shapeimage_1_link_29shapeimage_1_link_30shapeimage_1_link_31shapeimage_1_link_32shapeimage_1_link_33shapeimage_1_link_34

Gudmund Grov

Position

Lecturer in Computer Science

  1. Heriot-Watt University

Previously

  1. University of Edinburgh -- under Alan Bundy

  2. University of Newcastle [RA] -- under Cliff Jones

  3. Heriot-Watt University [RA & PhD] -- under Andrew Ireland & Greg Michaelson


Contact Details

Email:  G.Grov (at) hw (dot) ac (dot) uk

Phone: +44 (0) 131 451 3412

Address: Room G.49, Earl Mountbatten Building, Computer Science, School of Mathematical and Computer Sciences, Heriot-Watt University, Edinburgh, EH14 4AS


Organisation

  1. Co-organiser of WING’12

  2. Publicity chair for VSTTE’12 (Philadelphia)  and VSTTE’10 (Edinburgh)

  3. Co-organiser of SSFRR’10 summer school (Edinburgh,2010)

  4. Programme committee for PLMMS’10 (Paris) 

  5. Organiser of the AI4FM meetings [2010/2011]

  6. Web site coordinator for the Verified Software Initiative


Some Links

  1. [AI4FM project] [MRG -- Edinburgh]  [CSR -- Newcastle]  [DSG -- Heriot-Watt]  [VSI]

  2. [Event-B page]  [CORE project] [SEAR project] [Hume page]  [Isabelle page] [CS BibTeX]