The Verified Software Initiative: A Manifesto

被引：14
作者：
Hoare, C. A. R.
Misra, Jayadev [1 ]
Leavens, Gary T. [2 ]
Shankar, Natarajan [3 ]
机构：
[1] Univ Texas Austin, Dept Comp Sci, Austin, TX 78712 USA
[2] Iowa State Univ, Dept Comp Sci, Ames, IA USA
[3] SRI Int, Comp Sci Lab, Manlo Pk, CA USA
来源：
ACM COMPUTING SURVEYS | 2009年 / 41卷 / 04期
基金：
美国国家科学基金会;
关键词：
D O I：
10.1145/1592434.1592439
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
A team of researchers from SRI International Computer Science Laboratory has proposed a long-term research program toward the construction of error-free software systems. The research project, called the Verified Software Initiative, will make an effort to a comprehensive theory of programming that covers the features needed to build practical and reliable programs. It will focus on a coherent toolset that automates the theory and scales up to the analysis of industrial-strength software. It will also develop a collection of realistic verified programs that can replace unverified programs in existing service and continue to evolve in a verified state. Verification involves the rigorous demonstration of the correctness of software with respect to a specification of its intended behavior. It can be applied at all phases of the software lifecycle including design to maintenance.
引用
收藏
页数：8
相关论文
共 50 条
  • [11] Verified software: A grand challenge
    Jones, C
    O'Hearn, P
    Woodcock, J
    COMPUTER, 2006, 39 (04) : 93 - 95
  • [12] Verified trustworthy software systems
    Gardner, Philippa
    PHILOSOPHICAL TRANSACTIONS OF THE ROYAL SOCIETY A-MATHEMATICAL PHYSICAL AND ENGINEERING SCIENCES, 2017, 375 (2104):
  • [13] Verified Squared: Does Critical Software Deserve Verified Tools?
    Leroy, Xavier
    ACM SIGPLAN NOTICES, 2011, 46 (01) : 1 - 2
  • [14] What use is verified software?
    Rushby, John
    12TH IEEE INTERNATIONAL CONFERENCE ON ENGINEERING COMPLEX COMPUTER SYSTEMS, PROCEEDINGS, 2007, : 270 - 276
  • [15] Verified Squared: Does Critical Software Deserve Verified Tools?
    Leroy, Xavier
    POPL 11: PROCEEDINGS OF THE 38TH ANNUAL ACM SIGPLAN-SIGACT SYMPOSIUM ON PRINCIPLES OF PROGRAMMING LANGUAGES, 2011, : 1 - 2
  • [16] Sustainability Design and Software: The Karlskrona Manifesto
    Becker, Christoph
    Chitchyan, Ruzanna
    Duboc, Leticia
    Easterbrook, Steve
    Penzenstadler, Birgit
    Seyff, Norbert
    Venters, Colin C.
    2015 IEEE/ACM 37TH IEEE INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING, VOL 2, 2015, : 467 - 476
  • [17] A Manifesto for Energy-Aware Software
    Fonseca, Alcides
    Kazman, Rick
    Lago, Patricia
    IEEE SOFTWARE, 2019, 36 (06) : 79 - 82
  • [18] The ideal of verified software (Invited talk)
    Hoare, Tony
    COMPUTER AIDED VERIFICATION, PROCEEDINGS, 2006, 4144 : 5 - 16
  • [19] THE FMICS VIEW ON THE VERIFIED SOFTWARE REPOSITORY
    Arenas, Alvaro E.
    Bicarregui, Juan C.
    Margaria, Tiziana
    JOURNAL OF INTEGRATED DESIGN & PROCESS SCIENCE, 2006, 10 (04) : 47 - 54
  • [20] Automated test generation and verified software
    Rushby, John
    VERIFIED SOFTWARE: THEORIES, TOOLS, EXPERIMENTS, 2008, 4171 : 161 - 172
12345