SHF: Small: Driving Learning for Program Verification

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

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.