CRII: SHF: Optimal Interpolation for Efficient Proof Synthesis

软件现在几乎支配着我们生活的方方面面：从手表到股票市场，从恒温器到外科医生。这种扩散不太可能在短期内放缓;事实上，我们似乎只是见证了软件革命的开始。社会越来越依赖高度复杂和相互关联的软件系统，这使得软件安全、保密和隐私成为社会关注的头等大事。为了对复杂的软件系统进行形式化和数学化的推理，自动验证和程序分析技术在过去十年中被证明是强大的，这要归功于该领域的大量进步。然而，大多数非平凡的程序和正确性的利益仍然遥不可及的自动验证技术。该项目研究新的自动化软件验证技术和工具，这些技术和工具更有效，适用于更广泛的程序和属性。具体来说，该项目开发新的技术计算克雷格插值，这是逻辑手段，综合证明的正确性。重点是探讨问题的计算最佳插值-最简单的可能。这项工作的动机是观察到，简单的插值更有可能推广到正确性的证明。该项目的目标是为复杂程序和正确性属性的有效验证开发算法基础，从而扩展形式验证技术的适用性。

Software now dominates almost every aspect of our life: from wrist watches to the stock markets, and from thermostats to surgeons. And this proliferation is unlikely to slow down any time soon; in fact, it appears that we are merely witnessing the very beginning of the software revolution. Society is ever more reliant on highly complex and interconnected software systems, and this has made software safety, security, and privacy a first-class societal concern.To formally and mathematically reason about complex software systems, automated verification and program analysis techniques have proven powerful over the past decade, thanks to a plethora of advances in the area. However, most non-trivial programs and correctness properties of interest remain out of reach for automated verification techniques. The project investigates new automated software verification techniques and tools, that are more efficient and applicable to a wider range of programs and properties. Specifically, the project develops novel techniques for computing Craig interpolants, which are logical means for synthesizing proofs of correctness. The emphasis is on exploring the question of computing optimal interpolants---the simplest possible ones. The work is motivated by the observation that simpler interpolants are more likely to generalize to a proof of correctness. The goal of the project is to develop an algorithmic foundation for efficient verification of complex programs and correctness properties, thus expanding the applicability of formal verification techniques.