SHF: Small: Efficient Verification of Nonlinear Arithmetic

近几十年来，形式化方法在证明硬件和软件制品的性质方面取得了许多成功。然而，缺乏通用的有效方法来验证涉及非线性算术的设计--涉及整数乘法的算术--一直是验证方法在广泛应用中的有效性的主要障碍。在许多其他应用中，依赖于非线性算法的计算是CPU设计、密码学和用于高效存储数据以便于检索的结构的核心。本项目致力于实现包括非线性算法在内的硬件和软件设计的高效验证。这个项目探索了扩展当前最有效的验证方法类的方法，这些方法的核心是使用布尔可满足性(SAT)解算器来处理包括整数乘法的设计。研究人员已经证明，被猜测代表验证非线性算术的难度的整数乘法电路的某些性质可以在捕获最先进的SAT解算器能力的推理系统中有效地验证。该项目利用并扩展这些理论见解来开发实用方法，这些方法将在使用非线性算法的软件和硬件制品的广泛验证任务中获得成功。研究成果将在开放源码工具中广泛传播，供人们用于验证，从而产生具有更高可信度的软件和硬件，包括人们每天依赖的安全关键应用程序。

In recent decades, formal methods have produced many successes in proving properties of hardware and software artifacts. However, the lack of general efficient methods to verify designs that involve nonlinear arithmetic -- arithmetic that involves integer multiplication -- has been a major impediment to the effectiveness of verification methods in a broad array of applications. Among many other applications, computations that depend on nonlinear arithmetic are at the heart of CPU designs, cryptography, and structures for efficient storage of data for easy retrieval. This project is focused on achieving efficient verification of hardware and software designs that include nonlinear arithmetic. This project explores methods for extending the most widely effective class of current verification methods, which at their heart use Boolean satisfiability (SAT) solvers, to handle designs that include integer multiplication. The investigators have shown that certain properties of integer multiplication circuits that have been conjectured to be representative of the difficulty of verifying nonlinear arithmetic can be efficiently verified in systems of inference that capture the capabilities of state-of-the-art SAT solvers. This project leverages and extends these theoretical insights to develop practical methods that will succeed in a broad range of verification tasks for software and hardware artifacts that use nonlinear arithmetic. The research results will be widely disseminated in open source tools for people to use for verification leading to software and hardware with a higher level of trustworthiness, including in safety-critical applications that people rely on every day.