CAREER: UNITY: Bridging the Gap Between Program Analyzers and Deductive Verifiers via Abductive Reasoning

由于软件的普遍性和程序错误的破坏性，保证软件可靠性的技术现在比以往任何时候都更加重要。这个项目研究在表达性和自动化之间实现正确权衡的程序验证技术，从而允许对不同类型的软件进行验证。关键思想是通过自动合成合成证明中所需的引理，使用溯因推理尽可能地自动化正确性证明。另一个关键思想是自动诊断失败的证明尝试，并向用户提供建设性的反馈。该项目更广泛的影响是能够对有趣的属性进行大部分自动化的、用户友好的验证，这些属性很难使用传统的演绎验证器来证明，但也超出了全自动程序分析器的范围。另一个重要的目标是发现比今天使用测试和程序分析技术可以识别的更深、更细微的软件缺陷。

Due to the ubiquity of software and the increasingly disruptive nature of program bugs, techniques for guaranteeing software reliability are more important now than ever before. This project studies program verification techniques that achieve the right trade-off between expressiveness and automation, thereby allowing the verification of a diverse class of software. The key idea is to use abductive reasoning to automate the correctness proof as much as possible by automatically synthesizing lemmas needed in a compositional proof. Another key idea is to automatically diagnose failed proof attempts and provide constructive feedback to users.The broader impact of the project is to enable mostly-automated, user-friendly verification of interesting properties that are too hard to prove using traditional deductive verifiers but beyond the reach of fully-automated program analyzers. Another important goal is to uncover deeper and more subtle software defects than those that can be identified using testing and program analysis technology today.