Verified Squared: Does Critical Software Deserve Verified Tools?

被引:0
|
作者
Leroy, Xavier [1 ]
机构
[1] INRIA Paris Rocquencourt, Paris, France
关键词
Languages; Verification; FORMAL VERIFICATION; SYSTEM;
D O I
10.1145/1925844.1926387
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
The formal verification of programs have progressed tremendously in the last decade. Principled but once academic approaches such as Hoare logic and abstract interpretation finally gave birth to quality verification tools, operating over source code (and not just idealized models thereof) and able to verify complex real-world applications [6, 8, 15, 18]. In this talk, I review some of the obstacles that remain to be lifted before source-level verification tools can be taken really seriously in the critical software industry: not just as sophisticated bug-finders, but as elements of absolute confidence in the correctness of a critical application.
引用
收藏
页码:1 / 2
页数:2
相关论文
共 50 条
  • [1] Verified Squared: Does Critical Software Deserve Verified Tools?
    Leroy, Xavier
    [J]. POPL 11: PROCEEDINGS OF THE 38TH ANNUAL ACM SIGPLAN-SIGACT SYMPOSIUM ON PRINCIPLES OF PROGRAMMING LANGUAGES, 2011, : 1 - 2
  • [2] Verified software: Theories, tools and experiments
    Computing Laboratory, Oxford University, Wolfson Building, Parks Road, Oxford OX13QD, United Kingdom
    不详
    [J]. Int. J. Softw. Tools Technol. Trans., 6 (405-408): : 405 - 408
  • [3] TOTALLY VERIFIED SYSTEMS - LINKING VERIFIED SOFTWARE TO VERIFIED HARDWARE
    JOYCE, JJ
    [J]. LECTURE NOTES IN COMPUTER SCIENCE, 1990, 408 : 177 - 201
  • [4] Maintaining Verified Software
    Leslie-Hurd, Joe
    [J]. ACM SIGPLAN NOTICES, 2013, 48 (12) : 71 - 80
  • [5] Verified Software Toolchain
    Appel, Andrew W.
    [J]. PROGRAMMING LANGUAGES AND SYSTEMS, 2011, 6602 : 1 - 17
  • [6] Verified Software Units
    Beringer, Lennart
    [J]. PROGRAMMING LANGUAGES AND SYSTEMS, ESOP 2021, 2021, 12648 : 118 - 147
  • [7] Maintaining verified software
    Leslie-Hurd, Joe
    [J]. ACM SIGPLAN Notices, 2014, 48 (12): : 71 - 80
  • [8] Verified software: Theories, tools, experiments vision of a grand challenge project
    Hoare, Tony
    Misra, Jay
    [J]. VERIFIED SOFTWARE: THEORIES, TOOLS, EXPERIMENTS, 2008, 4171 : 1 - 18
  • [9] Verified software grand challenge
    Woodcock, Jim
    [J]. FM 2006: FORMAL METHODS, PROCEEDINGS, 2006, 4085 : 617 - 617
  • [10] The Verified Software Initiative: A Manifesto
    Hoare, C. A. R.
    Misra, Jayadev
    Leavens, Gary T.
    Shankar, Natarajan
    [J]. ACM COMPUTING SURVEYS, 2009, 41 (04)