New Handles on 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.