Verification system aims to guarantee software function

Dr Patricia Johann and Prof Neil Ghani, of Strathclyde’s Department of Computer and Information Sciences, aim to develop software that guarantees programs perform the computations they are designed to carry out.

This software aims to stop programs performing unintended tasks, thereby improving the reliability of safety-critical systems, such as those running nuclear facilities, aeroplanes, and credit card transactions.

Prof Ghani, co-investigator on the £440,000 EPSRC-funded project, said, ‘In an economy as relentlessly digital as the modern worldwide one – in which everything from toasters, to interpersonal communications, to global financial services are computerised – the need for formally-verified software cannot be overestimated.

‘Formal verification uses mathematical techniques to prove that programs actually perform the computations they are intended to perform – for example, that text editors really do save a file when a ‘save’ command is issued, or that automatic pilots really do correctly execute flight plans. Formal verification also ensures programs avoid performing unintended computations, such as leaking credit card details.