Satisfiability.jl: Satisfiability Modulo Theories in Julia
Emiko Soroka, Mykel J. Kochenderfer, Sanjay Lall
TL;DR
This paper addresses the need for a high-level, idiomatic Julia interface to SMT solvers, enabling convenient construction and solving of SMT formulae. It introduces Satisfiability.jl, which represents SMT formulae using types like $BoolExpr$, $IntExpr$, $RealExpr$, and $BitVectorExpr$, and automatically generates SMT-LIB commands. Key contributions include a Julia-centric API with @satvariable and @uninterpreted macros, operator extensions, and an interactive solving workflow via an InteractiveSolver and solver process integration. The work facilitates formal verification workflows in Julia by providing a bridge to SMT-LIB solvers, with demonstrated benchmarks and documentation to enable broader adoption.
Abstract
Satisfiability modulo theories (SMT) is a core tool in formal verification. While the SMT-LIB specification language can be used to interact with theorem proving software, a high-level interface allows for faster and easier specifications of complex SMT formulae. In this paper we present a novel open-source package for interacting with SMT-LIB compliant solvers in the Julia programming language.