Short CV I am a research associate within the AI4FM project, where the goal is to use AI to automate proofs within formal methods. I am currently employed by the EPSRC EP/E005713/1 The Integration and Interaction of Multiple Mathematical Reasoning Processes and EP/E035329/1 Trustworthy Ambient Systems (TrAmS)} platform grants at Edinburgh and Newcastle. From 1 April I will be employed on the EPSRC AI4FM project. I am also involved in the SEAR project, with Andrew Ireland and Teresa Llano at Heriot-Watt University. Here, the goal is to apply Lakatos style reasoning to Event-B models, using a technique we call reasoned modelling - which explores the interplay between reasoning & specification within Event-B. Previously, I was employed at Heriot-Watt as a RA on the CORE project (with Andrew Ireland and Ewen Maclean), which I am still involved in. Here, the focus is on automated correctness verification within separation logic. In my PhD (from Heriot-Watt University), I addressed functional correctness of Hume programs using Lamport’s TLA logic and Isabelle. I have also been employed on the EU-funded EmBounded (Hume) project at Heriot-Watt. I am the publicity chair for VSTTE’10 [Edinburgh, August 2010] I am co-organising the SSFRR’10 summer school [Edinburgh, August 2010] I am on the programme committee for PLMMS’10 [Paris, July 2010] Refereed Publications [bibtex] A. Ireland and G.Grov. Reasoned Modelling Critics: Turning Failed Proofs into Modelling Guidance. To appear in ABZ’10. A. Bundy, G. Grov and C. B. Jones. Learning from experts to aid the automation of proof search. In PreProceedings of 9th International Workshop on Automated Verification of Critical Systems (AVoCS’09) [pdf]. G. Grov and A. Ireland. Towards Automatic Property Discovery within Hume. In Proceedings of 2nd International Conference on Invariant Generation (Satellite Workshop of ETAPS 2009) [pdf]. G. Grov, G. Michaelson, C. Hermann, H-W. Loidl, S. Jost and K. Hammond. Hume Cost Analysis for Imperative Programs. In proceedings of 2009 International Conference on Software Engineering Theory and Practice [pdf]. G. Grov, R. Pointon, G. Michaelson and A. Ireland. Preserving Coordination Properties when Transforming Concurrent System Components. To appear in Coordination Models, Languages and Application track of 23rd Annual ACM Symposium on Applied Computing [pdf]. (full version [pdf]) G. Grov, G. Michaelson and A. Ireland. Formal Verification of Concurrent Scheduling Strategies using TLA. In proceedings of 13th International Conference on Parallel and Distributed Systems - 3rd IEEE International Workshop on Scheduling and Resource Management for Parallel and Distributed Systems. [pdf] G. Grov and G. Michaelson. Towards a Box Calculus for Hierarchical Hume. In Trends in Functional Programming, Volume 8. [pdf] 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 Programming. [pdf] 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 (doctoral symposium). [pdf] Non-Refereed Publications / Thesis / Technical Reports [bibtex] A.Bundy, G. Grov and C.B. Jones. An outline of a proposed system that learns from experts how to discharge proof obligations automatically. To appear in Schloss Dagstuhl proceedings on Refinement Based Methods for the Construction of Dependable Systems (2009) A.Ireland and G. Grov. Reasoned Modelling: Combining Proof and Modelling Patterns to Guide Systems Design. To appear in Schloss Dagstuhl proceedings on Refinement Based Methods for the Construction of Dependable Systems (2009) G. Grov, A. Ireland, M. Butler, A. Bundy and C. Jones. A Proposal for a Rodin Proof Planner & Reasoned Modelling Plug-in. In Proceeding of Rodin User and Developer Workshop 2009. [pdf] G. Grov. Reasoning about Correctness Properties of a Coordination Programming Language. PhD thesis, Heriot-Watt University, March 2009. [pdf (15 MB)] G. Grov. A Formal Account of Hume Scheduling. Heriot-Watt CS Technical Report (June ‘07) [pdf] G. Grov, A. Ireland, G. Michaelson and K. Hammond. Verifying Temporal Properties in HW-Hume. Technical Report (February ‘06) [pdf] G. Grov, A. Ireland and G. Michaelson. Model Checking HW-Hume. In Draft Proceedings of 5th International Symposium on Trends in Functional Programming (also published as a Heriot-Watt CS technical report). [pdf] G. Grov. Model Checking HW-Hume. MSc thesis (Heriot-Watt University) [ps (13 MB)] Selected Talks and Presentations AI4FM. Presented at Schloss Dagstuhl seminar on Refinement Based Methods for the Construction of Dependable Systems (Schloss Dagstuhl, Germany; September’09) [slides] A Proposal for a Rodin Proof Planner & Reasoned Modelling Plug-in. Presented at Rodin User and Developer Workshop (Southampton, UK; July’09) [slides] Towards Automatic Property Discovery within Hume. Presented at 2nd International Conference on Invariant Generation (Satellite Workshop of ETAPS 2009) (York, UK; March’09) [slides 4 up] Formal Verification of Concurrent Scheduling Strategies using TLA. Presented at Workshop on Scheduling and Resource Management for Parallel and Distributed Systems (Hsinchu,Taiwan; December ’07) [slides-4up] Towards a Box Calculus for Hierarchical Hume. Presented at Trends in Functional Programming (New York; April ’07) and Scottish Theorem Provers (Stirling; June ‘07) [slides-4up] Verifying the Correctness of Hume Programs. Presented at doctoral symposium of Automated Software Engineering (Long Beach,California; November ‘05) [slides 4up] Combining Algorithmic and Deductive Reasoning to Verify Hume Programs. Presented at CLAM-INKA-OMRS workshop (Nottingham; April ‘05) [slides] Model Checking HW-Hume. Presented at Scottish Theorem Provers (Edinburgh, October ‘04) and Trends in Functional Programming (Munich; November ‘04) [slides] Posters AI4FM: using AI to aid automation of proof search in Formal Methods. Internal review (Edinburgh; December’09) [poster.pdf] Preserving Coordination Properties when Transforming Concurrent System Components. Presented at 23rd Annual ACM Symposium on Applied Computing (Fortaleza,Brazil; March’08) [poster.pdf] Verified Transformations Guided by Static Analysis: The Hume Approach Towards Correct Software with Bounds on Time & Space. Poster presented at QEST’07 Graduate Symposium (Edinburgh; September’07) [poster.pdf | abstract.pdf] 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: 15 January 2010http://www.AI4FM.org/http://www.macs.hw.ac.uk/sear/http://www.macs.hw.ac.uk/~air/http://www.macs.hw.ac.uk/~mtl4/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/~eahm2/http://www.hume-lang.orghttp://www.embounded.orghttp://www.macs.hw.ac.uk/vstte10/Home.htmlhttp://dream.inf.ed.ac.uk/events/ssfrr-2010/http://dream.inf.ed.ac.uk/events/plmms-2010/Gudmunds_homepage_files/gudmund.bibGudmunds_homepage_files/avocs09.pdfGudmunds_homepage_files/wing09.pdfGudmunds_homepage_files/setp09.pdfGudmunds_homepage_files/abstract.pdfGudmunds_homepage_files/sac08.pdfGudmunds_homepage_files/srmpds07.pdfGudmunds_homepage_files/tfp07.pdfGudmunds_homepage_files/ifl2006.pdfGudmunds_homepage_files/ds03-grov.pdfGudmunds_homepage_files/gudmund_1.bibGudmunds_homepage_files/rodin09.pdfGudmunds_homepage_files/PhD-thesis.pdfGudmunds_homepage_files/scheduling.pdfGudmunds_homepage_files/hwhume.pdfGudmunds_homepage_files/hwhume_1.pdfGudmunds_homepage_files/dissertation.psGudmunds_homepage_files/Dagstuhl-AI4FM-09.pdfGudmunds_homepage_files/rodin09-handouts.pdfGudmunds_homepage_files/slides-4-up.pdfGudmunds_homepage_files/presentation-4up.pdfGudmunds_homepage_files/STP-June-2007-4up.pdfGudmunds_homepage_files/ase-doc-symp-05.pdfGudmunds_homepage_files/ciao-05-printouts.pdfGudmunds_homepage_files/printouts.pdfGudmunds_homepage_files/poster.pdfGudmunds_homepage_files/sac.pdfGudmunds_homepage_files/qest-poster.pdfGudmunds_homepage_files/abstract_1.pdfGudmunds_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_34shapeimage_1_link_35shapeimage_1_link_36shapeimage_1_link_37shapeimage_1_link_38shapeimage_1_link_39shapeimage_1_link_40shapeimage_1_link_41shapeimage_1_link_42shapeimage_1_link_43shapeimage_1_link_44

Gudmund Grov

Position

Research Associative

  1. •University of Edinburgh -- under Alan Bundy

  2. •University of Newcastle -- under Cliff Jones

Previously

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


Contact Details

Email:  ggrov (at) inf (dot) ed (dot) ac (dot) uk

Phone: +44 (0) 131 650 9004

Address: Rm. 202, Informatics Forum, 10 Crichton Street, Edinburgh EH8 9AB, UK


Research Interest

  1. •My main research interest is within automated reasoning and formal methods

  2. ... both at the design and source-code level

  3. ... as well as the interplay between reasoning & specification within formal methods


Some Relevant Links

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

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