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.