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 条
  • [21] 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
  • [22] Verified Software:: The real grand challenge
    Bharadwaj, Ramesh
    [J]. VERIFIED SOFTWARE: THEORIES, TOOLS, EXPERIMENTS, 2008, 4171 : 318 - 324
  • [23] Using CARE to construct verified software
    Lindsay, P
    Hemer, D
    [J]. FIRST IEEE INTERNATIONAL CONFERENCE ON FORMAL ENGINEERING METHODS, PROCEEDINGS, 1997, : 122 - 131
  • [24] The FMICS view on the verified software repository
    E-Science Centre, CCLRC Rutherford Appleton Laboratory, Chilton, Oxfordshire, United Kingdom
    不详
    [J]. J. Integr. Des. Process Sci, 2006, 4 (47-54):
  • [25] Developing Verified Software Using Leon
    Kuncak, Viktor
    [J]. NASA FORMAL METHODS (NFM 2015), 2015, 9058 : 12 - 15
  • [26] A Simple, Verified Validator for Software Pipelining
    Tristan, Jean-Baptiste
    Leroy, Xavier
    [J]. POPL'10: PROCEEDINGS OF THE 37TH ANNUAL ACM SIGPLAN-SIGACT SYMPOSIUM ON PRINCIPLES OF PROGRAMMING LANGUAGES, 2010, : 83 - 92
  • [27] Formally Verified Software in the Real World
    Klein, Gerwin
    Andronick, June
    Fernandez, Matthew
    Kuz, Ihor
    Murray, Toby
    Heiser, Gernot
    [J]. COMMUNICATIONS OF THE ACM, 2018, 61 (10) : 68 - 77
  • [28] Manufacturer initiative software
    Herstellerinitiative Software
    [J]. 2001, VDI Verlag GMBH
  • [29] Manufacturer initiative software
    Lange, K
    Bortolazzi, J
    Brangs, R
    Marx, D
    Wagner, G
    [J]. ELECTRONIC SYSTEMS FOR VEHICLES, 2001, 1646 : 183 - 199
  • [30] Text software initiative
    [J]. Archives des Sciences et Compte Rendu Seances de la Societe, 1993, 46 (02):
12345