Formal verification: will the seedling ever flower?

被引:2
作者
White, Neil [1 ]
Matthews, Stuart [1 ]
Chapman, Roderick [1 ]
机构
[1] Altran UK, 22 St Lawrence St, Bath BA1 1AN, Avon, England
来源
PHILOSOPHICAL TRANSACTIONS OF THE ROYAL SOCIETY A-MATHEMATICAL PHYSICAL AND ENGINEERING SCIENCES | 2017年 / 375卷 / 2104期
关键词
formal methods; software verification; proof; SPARK;
D O I
10.1098/rsta.2015.0402
中图分类号
O [数理科学和化学]; P [天文学、地球科学]; Q [生物科学]; N [自然科学总论];
学科分类号
07 ; 0710 ; 09 ;
摘要
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'.
引用
收藏
页数:14
相关论文
共 25 条
  • [1] Altran UK, 2011, INFORMED DES METH SP
  • [2] Barnes J, 2006, P 1 IEEE INT S SEC S
  • [3] INFORMATION-FLOW AND DATA-FLOW ANALYSIS OF WHILE-PROGRAMS
    BERGERETTI, JF
    CARRE, BA
    [J]. ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 1985, 7 (01): : 37 - 61
  • [4] An Automatable Formal Semantics for IEEE-754 Floating-Point Arithmetic
    Brain, Martin
    Tinelli, Cesare
    Rummer, Philipp
    Wahl, Thomas
    [J]. IEEE 22ND SYMPOSIUM ON COMPUTER ARITHMETIC ARITH 22, 2015, : 160 - 167
  • [5] Deciding floating-point logic with abstract conflict driven clause learning
    Brain, Martin
    D'Silva, Vijay
    Griggio, Alberto
    Haller, Leopold
    Kroening, Daniel
    [J]. FORMAL METHODS IN SYSTEM DESIGN, 2014, 45 (02) : 213 - 245
  • [6] Burns Alan, 2004, Ada Lett., VXXIV, P1, DOI [10.1145/997119.997120, DOI 10.1145/997119.997120]
  • [7] Chapman Roderick, 2014, Interactive Theorem Proving. 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014. Proceedings: LNCS 8558, P17, DOI 10.1007/978-3-319-08970-6_2
  • [8] Chapman R, 2016, DEBATE ARCHAEOL, P143
  • [9] Croxford M., 2005, J. Def. Softw. Eng, P5
  • [10] Deters Morgan, 2014, 2014 Formal Methods in Computer-Aided Design (FMCAD), DOI 10.1109/FMCAD.2014.6987586