Formal verification: will the seedling ever flower?. (4th September 2017)

• Record Type: Journal Article
• Authors: White, Neil; Matthews, Stuart; Chapman, Roderick
• Is Part Of: Philosophical transactions. Volume 375:Number 2104(2017)
• Publication Date: 2017-09-04
• Subjects: formal methods -- software verification -- proof -- SPARK; Physical sciences -- Periodicals; Engineering -- Periodicals; Mathematics -- Periodicals; 500
• DOI: 10.1098/rsta.2015.0402
• Languages: English
• ISSNs: 1364-503X

Abstract

Abstract : 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'.