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.