Inaugural Lecture

Safe and Secure Software Systems - An Automated Reasoning Perspective

Professor Andrew Ireland    BSc PhD CEng FBCS CITP

Abstract

Software is woven into the fabric of modern life - from communications, entertainment and consumer electronics, to finance, healthcare and national infrastructure. As well as significant economic and social benefits, the proliferation of software brings with it serious risks - system failures and security vulnerabilities. To combat these risks calls for rigorous methods that enable us to reason precisely about the correctness of a software system. Mathematical logic and formal reasoning provide the foundations for such methods. To be applicable on an industrial scale, however, requires computer assistance in the form of automated tools and techniques. In my lecture I will illustrate some automated reasoning techniques and their application to verifying the correctness software systems - both at the level of code as well as design. I will also highlight the broader context for what has become a renaissance in software verification - an area of research that has a long and distinguished history dating back over sixty years.

| Presentation | Video | Poster |

Biography

Andrew Ireland studied at the University of Stirling where he graduated with a first class honours degree in Computing Science and then went on to gain his PhD sponsored by a Carnegie Scholarship. After a Research Associate position at the then Department of Artificial Intelligence (University of Edinburgh), he became a lecturer in Computer Science at Heriot-Watt University in 1995, and was promoted to Professor in 2010. He is a founder member of the Dependable Systems Group at Heriot-Watt, and has attracted substantial research funding for his work in automated reasoning and automated software engineering. He is currently the Principal Investigator of an EPSRC Platform Grant which underpins basic research across a consortium of three research groups: Heriot-Watt, Edinburgh and Imperial College. He also has a strong track-record in terms of applied research; his industrial collaborators have included BAE Systems, QinetiQ and Altran Praxis. He has wide ranging experience in organising international workshops and conferences. Most recently he brought the international "Verified Software: Theories, Tools and Experiments" (VSTTE-10) conference to Heriot-Watt in 2010.