Satisfiability.jl: Satisfiability Modulo Theories inJulia

Theorem proving software is one of the core tools in formal verification, model checking, and synthesis.Modern provers solve satisfiability modulo theories (SMT) problems encompassing propositional logic, integer and real arithmetic, floating-point arithmetic, strings, and data structures such as bit vectors (De Moura & Bjrner, 2011).Additionally, new theories and heuristics are continually being developed, increasing the practical utility of SMT (Bjrner et al., 2023;Saouli et al., 2023).This paper introduces Satisfiability.jl,a package providing a high-level representation for SMT formulae including propositional logic, integer and real-valued arithmetic, and bit vectors in Julia (Bezanson et al., 2017).Satisfiability.jl is the first published package for SMT solving in idiomatic Julia, taking advantage of language features such as multiple dispatch and metaprogramming to simplify the process of specifying and solving an SMT problem.