Formal verification: will the seedling ever flower?
Author(s) -
Neil White,
S Matthews,
Roderick Chapman
Publication year - 2017
Publication title -
philosophical transactions of the royal society a mathematical physical and engineering sciences
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 1.074
H-Index - 169
eISSN - 1471-2962
pISSN - 1364-503X
DOI - 10.1098/rsta.2015.0402
Subject(s) - seedling , computer science , biology , botany
In one sense, formal specification and verification have been highly successful: techniques have been developed in pioneering academic research, transferred to software companies through training and partnerships, and successfully deployed in systems with national significance. Altran UK has been in the vanguard of this movement. This paper summarizes some of our key deployments of formal techniques over the past 20 years, including both security- and safety-critical systems. The impact of formal techniques, however, remains within an industrial niche, and while government and suppliers across industry search for solutions to the problems of poor-quality software, the wider software industry remains resistant to adoption of this proven solution. We conclude by reflecting on some of the challenges we face as a community in ensuring that formal techniques achieve their true potential impact on society. This article is part of the themed issue ‘Verified trustworthy software systems’.
Accelerating Research
Robert Robinson Avenue,
Oxford Science Park, Oxford
OX4 4GP, United Kingdom
Address
John Eccles HouseRobert Robinson Avenue,
Oxford Science Park, Oxford
OX4 4GP, United Kingdom