CAREER: Modular Verification of Software

0546170加州大学洛杉矶分校的Rupak Majudar.软件的模块化验证.编写正确的软件很难。我们确保软件可靠性的技术远远落后于我们对越来越复杂的系统的要求。与低级正确性要求(如正确的语法或类型的正确使用)不同，应用程序级属性目前不能指定或自动检查。测试仍然是确保与应用程序级别属性相关的软件质量的主要方法，然而，它并不是详尽的，而且在部署后经常会暴露出令人讨厌的错误。因此，能够合理而准确地自动检查大型软件系统的高级属性的分析的可用性将标志着我们开发更可靠软件的能力的重大进步。该项目利用了软件验证方面的最新进展，并探索了新的想法，以显著扩展现代验证工具的能力，以处理更大的程序和更复杂的属性。我们认为，在模型检查、谓词抽象和抽象精化等现有技术之上，模块化软件验证中的新技术将使可伸缩验证软件端到端属性的飞跃成为可能。虽然系统验证中模块化的基本原则已经知道了几十年，但它们还没有在程序分析工具中被广泛采用，因为没有一种按钮方法来完全通用地应用它们。我们通过研究以下广泛出现的验证模式来关注自动化模块验证的技术挑战。通过谓词类型在模型检查中更紧密地集成类型信息。自动合成指定行为要求的时间界面。将抽象数据类型集成到符号推理中。通过设计分解实现自动参数化验证。我们的研究将立即使任何迫切需要健壮性和可靠性的大型软件系统受益；我们将通过验证企业应用程序和高性能服务器的端到端属性来验证我们的研究，我们从这些应用程序和高性能服务器获得验证模式，这些属性超出了当前工具的范围。

ABSTRACT0546170Rupak MajumdarUniversity of California - Los Angeles,Modular Verification of Software MajumdarIntellectual Merits. Writing correct software is hard. Our techniques to ensure software reliabilitylag far behind our requirements for more and more complex systems. Unlike for lowlevel correctness requirements (such as correct syntax, or correct use of types), application level properties are currently not specifiable or automatically checkable. Testing remains the dominant methodology to ensure software quality with regard to application level properties, however, it is not exhaustive, and nasty bugs are often exposed post-deployment. Thus, the availability of analyses that can automatically check higher-level properties of large software systems soundly and precisely will mark a major advance in our ability to develop more reliable software. This project leverages recent advances in software verification and explores new ideas to significantly extend the capabilities of modern verification tools to handle larger programs and more complex properties. We contend that the leap to scalably verifying end-to-end properties of softwarewill be enabled by novel techniques in modular software verification, over and above existing techniques like model checking, predicate abstraction, and abstraction refinement. While the basic principles of modularity in system verification have been known for decades, they have not been widely adopted in program analysis tools because there is no push-button way to apply them in full generality. We focus on the technical challenges in automating modular verification by studying the following widely occurring verification patterns. Tighter integration of type information in model checking through predicated types. Automatically synthesizing temporal interfaces that specify behavioral requirements. Integration of abstract data types into symbolic reasoning. Automatic parameterized verification through design decomposition. Our research will immediately benefit any large software system where robustness and reliability are pressing concerns; we shall validate our research by verifying end-to-end properties of enterprise applications and high performance servers from which we derived the verification patterns and which are beyond the scope of current tools.