New Handles on Program Correctness

程序正确性的新处理

• 批准号: 0729011
• 负责人: Shafrira Goldwasser
• 金额: $ 30万
• 依托单位: Massachusetts Institute of Technology
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2007
• 资助国家: 美国
• 起止时间: 2007-09-01 至 2011-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0729011&HistoricalAwards=false
• 关键词: New; Handles; Program; Correctness

One of the main challenges of software engineering is verifying the correctness of software. In the eighties the methodology of program `result checking' and `result correcting' was introduced. This approach focuses on correctness of the code per input rather than full program verification.The current investigation will revisit the result checking and correcting methodology, emphasizing a general complexity theoretic approach rather than the function specific approach pursued earlier.The intellectual merit of the project is that it will broaden our understanding of how to design general purpose program checkers and correctors, teach methods to exploit fast heuristics without sacrificing correctness, and study, in depth, the relation between the property testing field and program checking and correcting. The project promises to have broad impact on the reliability ofsoftware.This research involves, the following directions:1. Characterize general {\it classes} of functions which posses efficient checkers and correctors.2. Introduce a new model for program checking and correcting in which the checker and correctorhave access to a short advice string in addition to the program to be checked and corrected. The advice-string is computed off-line ahead of on-line checking of programs. Such model allows treating more general function families than previously done. In particular, it allows the design of a single checker and corrector for many functions, where each individual function is associated with a different advice string.3. Pursue new measures of efficiency for program checkers and correctors which will circumvent some of the challenges which arise in the field. In the advice model, the length of the advice will be incorporated into the complexity of the checking procedure and may be traded with the number of on-line calls of the checker to the program to be checked.4. Harness the remarkable progress made in the field of property testing to the testing and correcting of programs.5. Explore how the notions of program testers and correctors may enable the convertion of fast heuristics into correct programs with improved average case running time.

软件工程的主要挑战之一是验证软件的正确性。八十年代引入了程序“结果检查”和“结果修正”的方法。这种方法关注的是每个输入代码的正确性，而不是完整的程序验证。当前的研究将重新审视结果检查和纠正方法，强调一般的复杂性理论方法，而不是前面所追求的功能特定方法。本课题的智力价值在于拓宽了我们对如何设计通用程序检查和校正器的认识，教授了在不牺牲正确性的情况下利用快速启发式的方法，并深入研究了性能测试领域与程序检查和校正之间的关系。该项目有望对软件的可靠性产生广泛的影响。本研究涉及以下几个方向：1。描述具有有效检查器和校正器的一般{\it类}函数。引入一种新的程序检查和纠错模型，在这种模型中，除了要检查和纠错的程序之外，检查人员和纠错人员还可以访问一个简短的建议字符串。建议字符串在程序在线检查之前离线计算。这种模型允许处理比以前更一般的函数族。特别是，它允许为许多函数设计单个检查器和校正器，其中每个单独的函数与不同的建议字符串相关联。为程序检查和校正人员寻求新的效率措施，这将规避该领域出现的一些挑战。在通知模型中，通知的长度将被纳入到检查程序的复杂性中，并且可以与检查人员对待检查程序的在线呼叫次数进行交换。利用性能测试领域取得的显著进展，对程序进行测试和修正。探索程序测试器和纠错器的概念如何能够将快速启发式转换为具有改进的平均案例运行时间的正确程序。