Document Open Access Logo

Bit-Precise Reasoning with Parametric Bit-Vectors

Authors Zvika Berger , Yoni Zohar , Aina Niemetz , Mathias Preiner , Andrew Reynolds , Clark Barrett , Cesare Tinelli

PDF HTML 5

Files

Thumbnail PDF
PDF
LIPIcs.SAT.2025.4.pdf
  • Filesize: 0.97 MB
  • 24 pages
HTML5 Logo HTML (experimental)
LIPIcs.SAT.2025.4.html

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Automated reasoning
  • Software and its engineering → Formal methods
Keywords
  • Satisfiability Modulo Theories
  • Bit-precise Reasoning
  • Parametric Bit-vectors

Metrics

Abstract

The SMT-LIB theory of bit-vectors is restricted to bit-vectors of fixed width. However, several important applications can benefit from reasoning about bit-vectors of symbolic widths, i.e., parametric bit-vectors. Recent work has introduced an approach for solving formulas over parametric bit-vectors, via an eager translation to quantified integer arithmetic with uninterpreted functions. The approach was shown to be successful for several applications, including the bit-width independent verification of compiler optimizations, invertibility conditions, and rewrite rules. We extend and improve that approach in several aspects. Theoretically, we improve expressiveness by defining a new theory of parametric bit-vectors that supports more operators and allows reasoning about the bit-widths themselves. Algorithmically, we introduce a lazy algorithm that avoids the use of uninterpreted functions and quantified axioms for them. Empirically, we show a significant improvement by implementing and evaluating our approach, and comparing it experimentally to the previous one.

Cite As Get BibTex

Zvika Berger, Yoni Zohar, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark Barrett, and Cesare Tinelli. Bit-Precise Reasoning with Parametric Bit-Vectors. In 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 341, pp. 4:1-4:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.SAT.2025.4

Author Details

Zvika Berger
  • Bar-Ilan University, Ramat Gan, Israel
Yoni Zohar
  • Bar-Ilan University, Ramat Gan, Israel
Aina Niemetz
  • Stanford University, CA, USA
Mathias Preiner
  • Stanford University, CA, USA
Andrew Reynolds
  • The University of Iowa, Iowa City, IA, USA
Clark Barrett
  • Stanford University, CA, USA
Cesare Tinelli
  • The University of Iowa, Iowa City, IA, USA

Funding

This research was supported in part by the Stanford Center for Automated Reasoning, the Stanford Center for Blockchain Research, Defense Advanced Research Projects Agency (DARPA) contract FA875024-2-1001, Israel Science Foundation (ISF) grant number 619/21, National Science Foundation (NSF) grant number 2303489, and a gift from Amazon Web Services.

Supplementary Materials

References

  1. Haniel Barbosa, Clark W. Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Ying Sheng, Cesare Tinelli, and Yoni Zohar. cvc5: A versatile and industrial-strength SMT solver. In TACAS (1), volume 13243 of Lecture Notes in Computer Science, pages 415-442. Springer, 2022. URL: https://doi.org/10.1007/978-3-030-99524-9_24.
  2. Clark Barrett, Pascal Fontaine, and Cesare Tinelli. The Satisfiability Modulo Theories Library (SMT-LIB). www.SMT-LIB.org, 2023. Google Scholar
  3. Clark Barrett, Pascal Fontaine, and Cesare Tinelli. The SMT-LIB Standard: Version 2.7. Technical report, Department of Computer Science, The University of Iowa, 2025. Available at www.SMT-LIB.org. Google Scholar
  4. Clark Barrett, A. Stump, and Cesare Tinelli. The SMT-LIB standard - version 2.0. In Proceedings of the 8th international workshop on satisfiability modulo theories, Edinburgh, Scotland,(SMT '10), 2010. Google Scholar
  5. Nikolaj S. Bjørner and Mark C. Pichora. Deciding fixed and non-fixed size bit-vectors. In TACAS, volume 1384 of Lecture Notes in Computer Science, pages 376-392. Springer, 1998. URL: https://doi.org/10.1007/BFB0054184.
  6. Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Ziyad Hanna, Zurab Khasidashvili, Amit Palti, and Roberto Sebastiani. Encoding RTL constructs for MathSAT: a preliminary report. Electronic Notes in Theoretical Computer Science, 144(2):3-14, 2006. URL: https://doi.org/10.1016/J.ENTCS.2005.12.001.
  7. Martin Brain, Florian Schanda, and Youcheng Sun. Building better bit-blasting for floating-point problems. In Tomás Vojnar and Lijun Zhang, editors, Tools and Algorithms for the Construction and Analysis of Systems - 25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Part I, volume 11427 of Lecture Notes in Computer Science, pages 79-98. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-17462-0_5.
  8. Raik Brinkmann and Rolf Drechsler. RTL-datapath verification using integer linear programming. In Proceedings of ASP-DAC/VLSI Design 2002. 7th Asia and South Pacific Design Automation Conference and 15h International Conference on VLSI Design, pages 741-746. IEEE, 2002. URL: https://doi.org/10.1109/ASPDAC.2002.995022.
  9. Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri, and Roberto Sebastiani. Invariant checking of NRA transition systems via incremental reduction to LRA with EUF. In Tools and Algorithms for the Construction and Analysis of Systems: 23rd International Conference, TACAS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, Part I 23, pages 58-75. Springer, 2017. URL: https://doi.org/10.1007/978-3-662-54577-5_4.
  10. Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri, and Roberto Sebastiani. Satisfiability modulo transcendental functions via incremental linearization. In Automated Deduction-CADE 26: 26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6-11, 2017, Proceedings, pages 95-113. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-63046-5_7.
  11. The Coq development team. The coq proof assistant reference manual version 8.9, 2019. URL: https://coq.inria.fr/distrib/current/refman/.
  12. Burak Ekici, Arjun Viswanathan, Yoni Zohar, Cesare Tinelli, and Clark W. Barrett. Formal verification of bit-vector invertibility conditions in Coq. In Uli Sattler and Martin Suda, editors, Frontiers of Combining Systems - 14th International Symposium, FroCoS 2023, Prague, Czech Republic, September 20-22, 2023, Proceedings, volume 14279 of Lecture Notes in Computer Science, pages 41-59. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-43369-6_3.
  13. Herbert Enderton. A mathematical introduction to logic. Elsevier, 2001. Google Scholar
  14. Florian Frohn and Jürgen Giesl. Satisfiability modulo exponential integer arithmetic. In IJCAR (1), volume 14739 of Lecture Notes in Computer Science, pages 344-365. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-63498-7_21.
  15. Aarti Gupta and Allan L. Fisher. Parametric circuit representation using inductive boolean functions. In CAV, volume 697 of Lecture Notes in Computer Science, pages 15-28. Springer, 1993. URL: https://doi.org/10.1007/3-540-56922-7_3.
  16. Aarti Gupta and Allan L. Fisher. Representation and symbolic manipulation of linearly inductive boolean functions. In ICCAD, pages 192-199. IEEE Computer Society / ACM, 1993. URL: https://doi.org/10.1109/ICCAD.1993.580055.
  17. Fuqi Jia, Rui Han, Pei Huang, Minghao Liu, Feifei Ma, and Jian Zhang. Improving bit-blasting for nonlinear integer constraints. In Proceedings of the 32nd ACM SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2023, pages 14-25, New York, NY, USA, 2023. Association for Computing Machinery. URL: https://doi.org/10.1145/3597926.3598034.
  18. Henry S. Warren Jr. Hacker’s Delight, Second Edition. Pearson Education, 2013. Google Scholar
  19. Hanna Lachnitt, Mathias Fleury, Leni Aniva, Andrew Reynolds, Haniel Barbosa, Andres Nötzli, Clark W. Barrett, and Cesare Tinelli. IsaRare: Automatic verification of SMT rewrites in Isabelle/HOL. In Bernd Finkbeiner and Laura Kovács, editors, Tools and Algorithms for the Construction and Analysis of Systems - 30th International Conference, TACAS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Part I, volume 14570 of Lecture Notes in Computer Science, pages 311-330. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-57246-3_17.
  20. Nuno P. Lopes, David Menendez, Santosh Nagarakatte, and John Regehr. Provably correct peephole optimizations with alive. In PLDI, pages 22-32. ACM, 2015. URL: https://doi.org/10.1145/2737924.2737965.
  21. Makai Mann, Amalee Wilson, Yoni Zohar, Lindsey Stuntz, Ahmed Irfan, Kristopher Brown, Caleb Donovick, Allison Guman, Cesare Tinelli, and Clark W. Barrett. Smt-Switch: A solver-agnostic C++ API for SMT solving. In SAT, volume 12831 of Lecture Notes in Computer Science, pages 377-386. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-80223-3_26.
  22. Leonardo de Moura and Sebastian Ullrich. The Lean 4 theorem prover and programming language. In André Platzer and Geoff Sutcliffe, editors, Automated Deduction - CADE 28, pages 625-635, Cham, 2021. Springer International Publishing. URL: https://doi.org/10.1007/978-3-030-79876-5_37.
  23. Alexander Nadel. Bit-vector rewriting with automatic rule generation. In Armin Biere and Roderick Bloem, editors, Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings, volume 8559 of Lecture Notes in Computer Science, pages 663-679. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-08867-9_44.
  24. Aina Niemetz and Mathias Preiner. Ternary propagation-based local search for more bit-precise reasoning. In FMCAD, pages 214-224. IEEE, 2020. URL: https://doi.org/10.34727/2020/ISBN.978-3-85448-042-6_29.
  25. Aina Niemetz and Mathias Preiner. Bitwuzla. In Constantin Enea and Akash Lal, editors, Computer Aided Verification - 35th International Conference, CAV 2023, Paris, France, July 17-22, 2023, Proceedings, Part II, volume 13965 of Lecture Notes in Computer Science, pages 3-17. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-37703-7_1.
  26. Aina Niemetz and Mathias Preiner. Correction: Ternary Propagation-Based Local Search for more Bit-Precise Reasoning. https://bitwuzla.github.io/data/fmcad2020/fmcad2020-correction.pdf, 2025.
  27. Aina Niemetz, Mathias Preiner, and Armin Biere. Propagation based local search for bit-precise reasoning. Formal Methods Syst. Des., 51(3):608-636, 2017. URL: https://doi.org/10.1007/S10703-017-0295-6.
  28. Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, and Cesare Tinelli. On solving quantified bit-vector constraints using invertibility conditions. Formal Methods Syst. Des., 57(1):87-115, 2021. URL: https://doi.org/10.1007/S10703-020-00359-9.
  29. Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar, Clark W. Barrett, and Cesare Tinelli. Towards bit-width-independent proofs in SMT solvers. In Pascal Fontaine, editor, Automated Deduction - CADE 27 - 27th International Conference on Automated Deduction, Natal, Brazil, August 27-30, 2019, Proceedings, volume 11716 of Lecture Notes in Computer Science, pages 366-384. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-29436-6_22.
  30. Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar, Clark W. Barrett, and Cesare Tinelli. Towards satisfiability modulo parametric bit-vectors. J. Autom. Reason., 65(7):1001-1025, 2021. URL: https://doi.org/10.1007/S10817-021-09598-9.
  31. Aina Niemetz, Mathias Preiner, and Yoni Zohar. Scalable bit-blasting with abstractions. In Arie Gurfinkel and Vijay Ganesh, editors, Computer Aided Verification - 36th International Conference, CAV 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part I, volume 14681 of Lecture Notes in Computer Science, pages 178-200. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-65627-9_9.
  32. Tobias Nipkow, Lawrence C Paulson, and Markus Wenzel. Isabelle/HOL: a proof assistant for higher-order logic, volume 2283 of Lecture Notes in Computer Science. Springer Science & Business Media, 2002. URL: https://doi.org/10.1007/3-540-45949-9.
  33. Andres Nötzli, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W Barrett, and Cesare Tinelli. Reconstructing fine-grained proofs of rewrites using a domain-specific language. In FMCAD, pages 65-74, 2022. URL: https://doi.org/10.34727/2022/ISBN.978-3-85448-053-2_12.
  34. Andres Nötzli, Andrew Reynolds, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Clark W. Barrett, and Cesare Tinelli. Syntax-guided rewrite rule enumeration for SMT solvers. In SAT, volume 11628 of Lecture Notes in Computer Science, pages 279-297. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-24258-9_20.
  35. Mark Christopher Pichora. Automated Reasoning about Hardware Data Types Using Bit-Vectors of Symbolic Lengths. PhD thesis, University of Toronto, CAN, 2003. AAINQ84686. Google Scholar
  36. Andrew Reynolds, Haniel Barbosa, Andres Nötzli, Clark W. Barrett, and Cesare Tinelli. cvc4sy: Smart and fast term enumeration for syntax-guided synthesis. In CAV (2), volume 11562 of Lecture Notes in Computer Science, pages 74-83. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-25543-5_5.
  37. Cesare Tinelli and Calogero G. Zarba. Combining decision procedures for sorted theories. In Jóse Júlio Alferes and João Leite, editors, Logics in Artificial Intelligence, pages 641-653, Berlin, Heidelberg, 2004. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-540-30227-8_53.
  38. Zhihong Zeng, Priyank Kalla, and Maciej Ciesielski. LPSAT: a unified approach to RTL satisfiability. In Proceedings Design, Automation and Test in Europe. Conference and Exhibition 2001, pages 398-402. IEEE, 2001. URL: https://doi.org/10.1109/DATE.2001.915055.
  39. Yoni Zohar, Ahmed Irfan, Makai Mann, Aina Niemetz, Andres Nötzli, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, and Cesare Tinelli. Bit-precise reasoning via int-blasting. In VMCAI, volume 13182 of Lecture Notes in Computer Science, pages 496-518. Springer, 2022. URL: https://doi.org/10.1007/978-3-030-94583-1_24.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact