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

职业：UNITY：通过归纳推理弥合程序分析器和演绎验证器之间的差距

• 批准号: 1453386
• 负责人: Isil Dillig
• 金额: $ 58.84万
• 依托单位: University of Texas at Austin
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2015
• 资助国家: 美国
• 起止时间: 2015-02-01 至 2020-12-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1453386&HistoricalAwards=false
• 关键词: CAREER; UNITY; Bridging; Gap; Between

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.

由于软件的普遍性和程序错误的破坏性越来越多，因此保证软件可靠性的技术比以往任何时候都更为重要。该项目研究计划验证技术在表达和自动化之间实现正确的权衡，从而允许验证各种类型的软件。关键的想法是使用绑架推理来自动合成构图证明中所需的引理，以尽可能多地自动化正确性证明。另一个关键思想是自动诊断出失败的证明尝试并向用户提供建设性的反馈。该项目的更广泛影响是启用大多数是自动化的，用户友好的验证有趣属性的验证这些属性，这些属性难以证明使用传统的演绎验证器，而不是超越完全自动化的计划分析者的范围。另一个重要的目标是与当今可以使用测试和程序分析技术确定的软件缺陷揭示更深入，更细微的软件缺陷。