SHF: Small: Model-Based Bit-Precise Reasoning

形式化方法越来越广泛地用于确保我们日常生活中所依赖的硬件和软件系统的正确性、安全性和安全性。许多现代验证工具依赖于推理引擎，推理引擎可以在机器算法级别上自动有效地推理系统属性。这些推理引擎，称为可满足模理论（SMT）解算器，可以证明该性质总是为真，或者提供一个反例，如果情况并非如此。大多数SMT求解器并不直接在字级进行推理，而是将问题编译成其位级布尔表示（位爆破），然后将其委托给可满足性（SAT）求解器。这种方法的可扩展性是有限的，而且，对SAT的编译消除了初始问题的高层结构，这使得获得简洁有用的推理工件变得非常困难。这些工件对于现代验证方法的可伸缩性是至关重要的，缺乏对获得它们的支持阻碍了位精确验证的进展。基于基于模型推理的最新进展，本项目开发了在实践中有效的位向量理论的新决策过程，利用词级推理，并为插值和泛化提供原生词级支持。新程序与现有技术正交，并探索了这些关键的新思想：(1)不依赖于爆破钻头的基于模型的推理；(2)支持不依赖于证明生成的插值；(3)支持不依赖于量词消除的泛化。

Formal methods are becoming more widely used to ensure correctness, safety, and security of the hardware and software systems we rely on in our daily lives. Many modern verification tools depend on reasoning engines that can automatically and effectively reason about system properties at the level of machine arithmetic. These reasoning engines, called satisfiability modulo theories (SMT) solvers, can prove that the property is always true, or provide a counter-example if this is not the case. Most SMT solvers do not reason directly at the word-level but, instead, compile the problem into its bit-level Boolean representation (bit-blasting) and then delegate it to a satisfiability (SAT) solver. The scalability of this approach is limited and, moreover, the compilation to SAT eliminates the high-level structure of the initial problem, which makes obtaining concise and useful reasoning artifacts very difficult. These artifacts are crucial for scalability of modern verification methods, and the lack of support for obtaining them hinders progress in bit-precise verification. Based on recent advances in model-based reasoning this project develops novel decision procedures for the theory of bit-vectors that are effective in practice, take advantage of word-level reasoning, and provide native word-level support for interpolation and generalization. The new procedures are orthogonal to existing techniques, and explores these key novel ideas: (1) model-based reasoning that does not rely on bit-blasting; (2) support for interpolation that does not rely on proof generation; and (3) support for generalization that does not rely on quantifier elimination.