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.