Talk: 12:35-13:20 (English)
Analyzing Programs with SMT Solvers
Have you ever wanted to prove non-trivial properties of your programs automatically? It’s actually practical with modern SMT solvers like Z3! I’ll walk you through how we can compile a program to an SMT formula and how we can use that formula to do bounded verification—checking assertions in our code statically or comparing a program against an executable specification. This technique is tricky in general purpose programming, but works wonders for domain-specific languages.
Tikhon Jelvis
I picked up Haskell as my first functional language on a whim, and it’s stuck with me ever since. I’ve worked with other functional languages too—a compiler in Racket, a backend service in OCaml—but now I’m back in the Haskell world, working on Target’s supply chain optimization team. Apart from programming in Haskell and giving talks, I also actively write about Haskell and programming on Quora and help organize local meetups and events like BayHac.
