Certified Decision Procedures for Width-Independent Bitvector Predicates

Siddharth Bhat

doi:10.1145/3763148

Certified Decision Procedures for Width-Independent Bitvector Predicates

2025-10-01

0

PRE

AI

DOI：10.1145/3763148

原文求助

摘要

En 中文

位向量是自动推理的基础。少数交互式定理证明器（ITP），如Lean，通过位爆破（bitblasting）对固定宽度的位向量谓词的判定提供了强力支持。然而，即使是这些ITP对与宽度无关的位向量谓词提供的自动化支持也很少。为了填补这一空白，我们在Lean中贡献了新颖的、机械化的判定过程，用于与宽度无关的位向量谓词。判定与宽度无关的位向量理论片段的经典算法可以从模型检测（model checking）的角度来看待，其中公式对应于一个自动机，而公式的正确性是一种安全属性。然而，我们目前无法在机械化证明中使用这种视角，因为不存在可执行、快速且形式上经过验证的模型检测算法，这些算法可以从ITP内部交互式地使用。为了填补这一空白，我们机械化实现了模型检测文献中的关键算法：k-归纳法、自动机可达性、自动机空性检测以及自动机最小化。利用这些机械化的算法，我们贡献了可扩展的、机械化的判定过程，用于与宽度无关的位向量谓词。此外，对于出现在去混淆（deobfuscation）文献中的算术运算和按位运算混合的受控片段，我们机械化了一个近期的高效算法（MBA-Blast），该算法在这一片段上的表现优于更通用的过程。最后，我们在经典的编译器问题基准上评估了我们的判定过程，例如《Hacker's Delight》和LLVM的窥孔优化器，以及程序混淆的等价性检查问题。我们的工具解决了《Hacker's Delight》中的100%，我们其中的两个工具解决了去混淆数据集中的100%，并且解决了从LLVM的窥孔重写测试套件中提取的窥孔重写的最高27%。我们新的判定过程为交互式定理证明器中的与宽度无关的位向量推理提供了一键式体验，并且，更广泛地说，为快速、形式上经过验证的模型检测的基础算法铺平了道路。

Keyword:

bitvector

decision procedure

model checking

automata

Lean

Certified Decision Procedures for Width-Independent Bitvector Predicates

摘要

期刊

机构

引用论文