Satisfiability.jl: Satisfiability Modulo Theories in Julia
Emiko Soroka, Mykel J. Kochenderfer, Sanjay Lall
TL;DR
This paper introduces Satisfiability.jl, an open-source Julia package that provides a high-level interface for interacting with SMT-LIB compliant solvers, facilitating formal verification tasks.
Contribution
The paper presents a novel Julia package that simplifies and accelerates the specification and interaction with SMT solvers for formal verification.
Findings
Enables easier specification of SMT formulas in Julia
Provides faster interaction with SMT solvers
Open-source and compatible with SMT-LIB standards
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Formal Methods in Verification · Security and Verification in Computing