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.
This session is held on in Talks #2