I am a Principal Scientist at the Norwegian Defence Research Establishment (FFI) and an Associate Professor at the University of Oslo. Before that I worked as an Assistant Professor (Lecturer) in Computer Science at Heriot-Watt University in Edinburgh, UK. I have also worked at the University of Edinburgh (School of Informatics) and Newcastle University.
Awards, honours & professional memberships
SICSA Early Career Industrial Fellowship
Fellow of the Higher Education Academy
Member of EPSRC Peer Review Associate College
Paper `Towards Formal Proof Script Refactoring' won best paper award at MKM 2011
Paper `Tactics for the Dafny Program Verifier' nominated for EATCS award (ETAPS 2016)
Paper 'Towards Data-Driven Autonomous Cyber Defence for Military Unmanned Vehicles With Autonomous Capabilities - Threats & Attacks' nominated for best paper at MILCOM 2022.
PhD thesis, entitled Reasoning About Correctness Properties of a Coordination Language (March 2009) [link] nominated for BCS distinguished dissertation award
Distinction awarded for MSc (2004) [link, PDF]
Several personal grants and awards: James Watt Scholarship, Knut Hamsuns minnefond, Lise og Arnfinn Hejes fond, Petter Dass‘ stipendiefond, Ludvig Daae Løvestad Legat, Johan Helmich Janson og Marcia Jansons Legat, Direktør Halvor B. Holtas Legat ved NTNU, Nansenfondet og de dermed forbundne fond (Det Norske Videnskaps-Akademi)
Useful Links
The researcher's bible by Alan Bundy and others
Useful advice on how to read a paper by S. Keshav
Collection of Bibtex entries and Google Scholar
Some tips for teaching computer science
Phd supervision
Colin Farquhar (Heriot-Watt 2022). Thesis: Meta-Interpretive Learning Of Proof Strategies
Daniel Raggi (Edinburgh 2016). Thesis: Searching the space of representations: reasoning through transformations for mathematical problem solving [PDF]
Rajiv Murali (Heriot-Watt 2016). Thesis: A Rigorous Approach to Combining Use Case Modelling and Accident Scenarios [PDF]
Yuhui Lin (Edinburgh 2015). Thesis: The Use of Rippling to Automate Event-B Invariant Preservation Proofs. [PDF]
Iain Whiteside (Edinburgh 2013). Thesis: Refactoring Proofs. [PDF]
Maria Teresa Llano Rodriguez (Heriot-Watt 2012;). Thesis: Invariant Discovery and Refinement Plans for Formal Modelling in Event-B [PDF]
Events
Dafny Autumn School (Edinburgh, 2016 - with Rustan Leino)
Co-organiser of AVoCS 2015
Co-organiser of AI4FM 2015
Co-organiser of AI4FM 2014 (Singapore - at FM 2014)
Co-organiser of AI4FM 2013 (Rennes - at ITP 2013)
Co-organiser of CIAO 2013 (The Burn, Scotland)
Two-day course on the Isabelle theorem prover in May 2013 (Edinburgh - with Makarius Wenzel and Grant Passmore)
Co-organiser of WING 2012 (Manchester)
Publicity chair for VSTTE 2012 (Philadelphia)
Organiser of AI4FM 2011 (Edinburgh)
Publicity chair for VSTTE 2010 (Edinburgh)
Co-organiser of SSFRR 2010 summer school (Edinburgh,2010)
Co-organiser of AI4FM 2010 (Newcastle)
Organiser of the Scottish Theorem Proving (STP) seminar series
Editorial
Science of Computer Programming Special Issue on Automated Verification of Critical Systems (AVoCS 2015), Volume 148, Pages 1-212 (15 November 2017), Guest editors: Gudmund Grov and Andrew Ireland.
Science of Computer Programming Special Issue on Invariant Generation, Volume 93, Part B, Pages 87-182, Guest editors: Gudmund Grov and Thomas Wies.
Proceedings of AVoCS 2015 & PreProceedings of AVoCS [link]
Contributions of AI4FM 2015, AI4FM 2014 & AI4FM 2013 [link]
PC member
AVoCS 2015 (co-chair)
WING 2012 (co-chair)