Despite the crucial need for formal safety and security verification of programs, discovering loop invariants remains a significant challenge. Static analysis is a primary technique for inferring loop invariants but often relies on substantial assumptions about underlying theories. Data-driven methods supported by dynamic analysis and machine learning algorithms have shown impressive performance in inferring loop invariants for some challenging programs. However, state-of-the-art data-driven techniques do not offer theoretical guarantees for finding loop invariants. We present a novel technique that leverages the simulated annealing (SA) search algorithm combined with SMT solvers and computational geometry to provide probabilistic guarantees for inferring loop invariants using data-driven methods. Our approach enhances the SA search with real analysis to define the search space and employs parallelism to increase the probability of success. To ensure the convergence of our algorithm, we adapt e-nets, a key concept from computational geometry. Our tool, DLIA2, implements these algorithms and demonstrates competitive performance against state-of-the-art techniques. We also identify a subclass of programs, on which we outperform the current state-of-the-art tool GSpacer.

翻译：尽管对程序进行形式化安全与安全验证的需求至关重要，但发现循环不变式仍然是一个重大挑战。静态分析是推断循环不变式的主要技术，但通常依赖于对底层理论的重大假设。由动态分析和机器学习算法支持的数据驱动方法在推断某些具有挑战性程序的循环不变式方面已展现出令人印象深刻的性能。然而，最先进的数据驱动技术并未为找到循环不变式提供理论保证。我们提出了一种新颖的技术，该技术利用模拟退火搜索算法，结合SMT求解器和计算几何，为使用数据驱动方法推断循环不变式提供概率保证。我们的方法通过实分析来增强SA搜索以定义搜索空间，并利用并行性来提高成功概率。为确保我们算法的收敛性，我们采用了计算几何中的一个关键概念——e-网。我们的工具DLIA2实现了这些算法，并展示了与最先进技术相比具有竞争力的性能。我们还确定了一类程序子集，在该子集上我们的表现优于当前最先进的工具GSpacer。