Scholarlink

PolySAT is a word-level decision procedure supporting bit-precise SMT reasoning over polynomial arithmetic with large bit-vector operations. Addressing challenges of verified software, PolySAT integrates the theoretical development of SMT-based calculi with a proof of concept implementation and empirical evaluation. The PolySAT calculus extends conflict-driven clause learning modulo theories with two key components: (i) a bit-vector plugin to the equality graph, and (ii) a theory solver for bit-vector arithmetic with non-linear polynomials. PolySAT implements dedicated procedures to extract bit-vector intervals from polynomial inequalities. For conflict analysis and resolution, PolySAT comes with on-demand lemma generation over non-linear bit-vector arithmetic. PolySAT is integrated into the SMT solver Z3 and has applications in model checking and smart contract verification where bit-blasting techniques on multipliers/divisions do not scale.

错误：搜索内容不能为空，请输入英文关键词
错误：关键词超出字数限制，请精简
高级检索

PolySAT: Word-level Bit-vector Reasoning in Z3

  • 会议论文

  • 发表日期：

    2025年

查看全文
  • Jakob Rath,
  • Clemens Eisenhofer,
  • Daniela Kaufmann,
  • Nikolaj Bjørner,
  • Laura Kovács

摘要

PolySAT is a word-level decision procedure supporting bit-precise SMT reasoning over polynomial arithmetic with large bit-vector operations. Addressing challenges of verified software, PolySAT integrates the theoretical development of SMT-based calculi with a proof of concept implementation and empirical evaluation. The PolySAT calculus extends conflict-driven clause learning modulo theories with two key components: (i) a bit-vector plugin to the equality graph, and (ii) a theory solver for bit-vector arithmetic with non-linear polynomials. PolySAT implements dedicated procedures to extract bit-vector intervals from polynomial inequalities. For conflict analysis and resolution, PolySAT comes with on-demand lemma generation over non-linear bit-vector arithmetic. PolySAT is integrated into the SMT solver Z3 and has applications in model checking and smart contract verification where bit-blasting techniques on multipliers/divisions do not scale.