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

这个I-Corps项目探索了使用正式程序转换来提高商业软件质量的潜力。这个I-Corps项目更广泛的影响/商业潜力是使用自动程序转换技术，可以显着提高开发人员的生产力和软件质量。该技术通过自动检测和修复错误和其他软件问题来提高软件质量，使开发人员能够专注于其他领域，从而提高他们的生产力。故障修复对于避免软件错误，更一般地说，对于保持高软件质量至关重要。自动修复技术将使开发人员能够轻松且一致地避免整个错误和软件质量问题。从长远来看，这种自动程序转换系统的广泛使用可能会减少威胁生命和财产的错误。目前的软件故障修复实践是通过手工编写的自定义脚本来自动修复。然而，这是一个容易出错的练习，需要非常大的开发工作量。这个团队的方法是通过将修复表达为正式的程序转换规则来自动化修复。形式规则是强大的，允许复杂的修复，并在底层编程语言中表达。因此，它们很容易被开发人员理解。底层技术是K框架，它作为几种广泛使用的编程语言（包括JavaScript、Java和C）的规范和验证基础结构已经取得了成功。最近的结果表明，K框架也可以成功地用于自动程序转换。

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.