Invited Talk: Challenges in Bit-Vector Reasoning
                                Mathias Preiner1
                                1
                                    Stanford University


                                                                         Abstract
                                                                         The theory of fixed-size bit-vectors in Satisfiability Modulo Theories is essential in bit-precise reasoning
                                                                         applications. The dominant state-of-the-art approach for solving bit-vector formulas is a technique
                                                                         called bit-blasting, an eager reduction of bit-vectors to SAT. While surprisingly efficient in practice,
                                                                         bit-blasting may not scale for large bit-vectors or if bit-vector arithmetic is involved. In this talk, I will
                                                                         highlight challenges in reasoning over bit-vectors and discuss the current state of bit-level and word-level
                                                                         approaches.




                                SMT 2024: 22st International Workshop on Satisfiability Modulo Theories July 22–23, 2024, Montreal Canada
                                $ preiner@cs.stanford.edu (M. Preiner)
                                                                       © 2024 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
                                    CEUR
                                    Workshop
                                    Proceedings
                                                  http://ceur-ws.org
                                                  ISSN 1613-0073
                                                                       CEUR Workshop Proceedings (CEUR-WS.org)




CEUR
                  ceur-ws.org
Workshop      ISSN 1613-0073
Proceedings