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
基金
美国国家科学基金会;
关键词
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 条