SHF: Small: Driving Learning for Program Verification

SHF：小型：推动程序验证的学习

• 批准号: 1525936
• 负责人: Aarti Gupta
• 金额: $ 46.37万
• 依托单位: Princeton University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2015
• 资助国家: 美国
• 起止时间: 2015-09-01 至 2019-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1525936&HistoricalAwards=false
• 关键词: SHF; Small; Driving; Learning; Program

Program verification has broad applications, from ensuring safety of mission-critical software to improving program robustness and programmer productivity. Automatic program verification techniques employ various forms of learning to enhance scalability on large programs. These include deductive learning in modern logic-based solvers and learning from counterexamples in abstraction refinement procedures. Modular verification is essential for scaling verification to large software, and concurrent program verification is critical due to the wide prevalence of multi-core hardware. This project develops techniques for learning inductive invariants for modular verification in a teacher-learner setting. The research objectives include studying suitable languages of invariants at procedure boundaries, identifying requirements for progress in learning, and developing effective techniques for guiding the learner. The project also addresses verification of concurrent programs, where learning over different event sequences is performed by dynamic and predictive analysis over program traces. The goal is to drive the learning toward unexplored program behaviors by automatically generating test inputs. The research objectives include studying new trace abstractions and coverage metrics for concurrent programs, and developing techniques for coverage-guided test generation. The methods for driving learning include directed testing to target specific scenarios relevant for learning. Beyond these specific contributions, the results will provide insights on applying machine learning techniques in combination with static and dynamic analysis for advancing program verification. The project includes development of educational material, tools, and benchmarks that will be made publicly available.

程序验证具有广泛的应用，从确保关键任务软件的安全性到提高程序的健壮性和程序员的生产力。自动程序验证技术采用各种形式的学习来增强大型程序的可伸缩性。这包括现代基于逻辑的解算器中的演绎学习和抽象提炼过程中的反例学习。模块化验证对于扩展到大型软件的验证是必不可少的，而并发程序验证由于多核硬件的广泛流行而变得至关重要。该项目开发了在教师-学习者环境中学习模块化验证的归纳不变量的技术。研究目标包括研究过程边界上的不变量语言，识别学习过程的进步要求，以及开发有效的指导学习者的技术。该项目还处理并发程序的验证，其中通过对程序跟踪的动态和预测分析来执行对不同事件序列的学习。目标是通过自动生成测试输入，将学习推向未探索的程序行为。研究目标包括研究新的跟踪抽象和并发程序的覆盖度量，以及开发覆盖引导测试生成的技术。驾驶学习的方法包括针对与学习相关的特定场景的定向测试。除了这些具体的贡献之外，研究结果还将提供将机器学习技术与静态和动态分析相结合的见解，以推进程序验证。该项目包括将公开提供的教育材料、工具和基准的开发。