Andrew Ireland
Professor Andrew Ireland
School of Mathematical and Computer Sciences
Earl Mountbatten Building (Room G57)
Heriot-Watt University
Edinburgh EH14 4AS 
Tel:   +44 (0)131 451 3409
Fax:   +44 (0)131 451 3327

| Publications | Conferences | MACS | Room Booking | HW | FSS | Links | BBC | Rippling | Bibtex | Dictionary | Gmail | Google Translate | WebMail | Google | VISION | PURE | BT Yahoo | Staff Portal | BBC Bitesize | ResearchFish | Riddell Sketch Book | CS Man Sys | PURE | CS Wiki | CS CW MOD | MACS Project System | CS Share Point | WorkTribe | KeyServer |

My area of research is Automated Reasoning and Formal Methods, I work within the Dependable Systems Group at Heriot-Watt University. I am also a member of the Mathematical Reasoning Group at the University of Edinburgh. If you are interested in Automated Reasoning then you might find the Scottish Theorem Proving seminar series of interest. I am a member of IFIP WG 1.9/2.15 Verified Software. My Inaugural Lecture can be accessed here.

Research Interests

My research interests lie in the development of automated reasoning techniques that support the construction of safe and secure software intensive systems – from requirements through to coding. Building scalable automated reasoning tools requires an integration of techniques. I am particularly interested in combining static (i.e. theorem proving) and dynamic analysis (i.e. animation and execution logs). I am interested in approaches where there is a strong cooperation between complementary techniques. That is, where individual techniques combine their strengthens, but crucially compensate for each other's weaknesses through the communication of partial results and failures. A recurring theme within my research is the productive use of failure – using the analysis of a failed proof attempt to automate the synthesis of creative steps, e.g. missing properties that are required in order to establish the correctness of a system. I see such automation as improving the creativity and productivity of an engineer. To promote accessibility, I seek where possible to embed my work within conventional tools and methodologies.

Keywords: automated reasoning; meta-level reasoning; formal modelling and refinement; verification and synthesis; productive use of failure; combining animation with theory formation; problem frames; combining informal and formal modelling; safety and security; embeded formal methods.

I am interested in supervising PhD, MSc and BSc projects in the broad areas described above.

Research Projects

Details of my completed research projects can be found here.

Conferences and Workshops

Details of conferences and workshops that I have been involved in can be found here.


Rigorous Methods for Software Engineering (F21RS/F20RS) and Software Design (F28SD).