Using Z3 to Analyze and Verify Programs

Compose Conference · Talk · 44 min · 2016 · YouTube title: Analyzing Programs with Z3

Why it's here

HN lists it among the practical entry points for learning Z3 and formal verification.

What it covers

Tikhon Jelvis's Compose Conference talk on using the Z3 SMT solver to analyze and verify programs, including checking invariants with bounded loops. He demonstrates verifying programs in a small language by compiling them to Z3.