PickVidsAnalyzing Programs with Z3
Why it was recommended
the best one I've found as an entry point was the approach they use in Cryptol
Recommendationbuckie · Original
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. It is for someone who already knows the basic terms and wants the next step.
Video details
- Channel
- Compose Conference
- Length
- 43 min 31 sec
- Year
- 2016