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.