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.
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.