Skip to main content
BOB 2019

Logo of BOB 2019 BOB 2019

22nd March 2019

Berlin, Germany

Part of the BOB series

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