Analyzing Programs with SMT Solvers - Tikhon Jelvis - FUN OCaml 2025

Analyzing Programs with SMT Solvers Tikhon Jelvis (Semgrep) ABSTRACT We can use SMT solvers like Z3 to analyze programs and answer difficult questions about our code. By generating and solving complex constraints, we can improve error message localization, attack cryptographic protocols, check refinement types, search for proofs, verify invariants, compare programs against specifications or even synthesize code. Z3 is the goto state-of-the-art SMT solver, available under and open source license and has a first-class OCaml library. In this talk, I'll walk through a simple OCaml program to generate SMT constraints that represent a bounded model of programs in a simple imperative language. Algebraic data types and pattern matching are a perfect fit for this kind of work. Session page: https://fun-ocaml.com/2025/analyzing-... Connect with FUN OCaml: Twitter: https://x.com/FunOCaml Bluesky: https://bsky.app/profile/fun-ocaml.com #ocaml --- Big Thanks(TM) go to our generous sponsors who made FUN OCaml possible! Octra Labs - https://octra.org/ - Platinum Sponsor Ahrefs - https://ahrefs.com/ - Platinum Sponsor Dialo - https://dialo.ai/ - Gold Sponsor LexiFi - https://www.lexifi.com - Bronze Sponsor Jane Street - https://www.janestreet.com/ - Bronze Sponsor LightSource - Volunteer / Organizer Commitment Tarides - Volunteer / Organizer Commitment