HackerTube / Video
Analyzing Programs with Z3
Compose Conference
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.
HN lists it among the practical entry points for learning Z3 and formal verification.
3 Hacker News mentions · 2016–2021