I-Corps: Automatic Formal Program Transformation for Improving Software Quality

点击翻译按钮获取中文摘要

This I-Corps project explores the potential of using formal program transformation for improving commercial software quality. The broader impact/commercial potential of this I-Corps project is the use of an automatic program transformation technology which can significantly improve developer productivity and software quality. The technology improves software quality by automating the detection and fixing of bugs and other software issues, freeing developers to focus on other areas thus increasing their productivity. Fault-fixes are crucial for avoiding software bugs and, more generally, for maintaining high software quality. The automatic fixing technology will allow developers to easily and consistently avoid entire classes of bugs and software quality problems. In the long term, widespread use of this automatic program transformation system may result in fewer bugs that threaten life and property.The current practice in software fault repair is to automate fixes through custom scripts written by hand. However, this is an error-prone exercise and requires a very large development effort. This team's approach is to automate the fixes by expressing them as formal program transformation rules. The formal rules are powerful, allowing complex fixes, and are expressed in the underlying programming language. Consequently, they are easy to comprehend by developers. The underlying technology is the K framework, which has been successful as a specification and verification infrastructure for several widely-used programming languages, including JavaScript, Java, and C. Recent results indicate the K framework can also be used successfully for automatic program transformation.