Analyzing Programs with Z3
Why Hacker News recommends it
HN lists it among the practical entry points for learning Z3 and formal verification.
What it is
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.
Recommended by 2 HN commenters across 2 different months, 2016 to 2021.
What Hacker News said
Recommends tikhonj · 2016-08 · on “Z3 SMT solver interactive tutorial”
If you want a fun example of using Z3, I gave a talk recently that walks you through verifying programs in a tiny little imperative language by compiling them to Z3 formulas. It's easier than it sounds! It was recorded [1] and I have example code and additional resources (papers, etc) on my site [2]. [1]: [this video] [2]: [LINK] If you want to do more, you can extend the same process to synthesizing programs, not just verifying them. It doesn't scale too far, but otherwise it's like magic.
Recommends buckie · 2017-07 · on “Show HN: Dharma – Programmable Peer-To-Peer Loans Using Ethereum Smart Contracts”
### FV Resources These are few and far between. My paper on it is soup to nuts for how we do it in Pact which, while technical, should be somewhat approachable for most devs to grasp (I tried at least -- representing a program as equations is just an abstract concept). Until it comes out, the best one I've found as an entry point was the approach they use in Cryptol: [this video] . Cryptol, generally is a great project to look to for guidance. We're not going with the interactive approach. An EDSL in the docstrings is our approach so that you can pull a contract from the chain (pact is interpreted so the code on chain is the code that executes... well after it gets inlined and validated) and do t
Cites philzook · 2021-01 · on “Software Verification and Analysis Using Z3”
These are other good resources: - rise4fun [LINK] - [LINK] - Programming Z3 - [LINK] - Nikolaj Bjorner's tutorial [LINK] - Hakank's examples [LINK] - Yurichev's book "SMT by Example" [LINK] - [LINK] - [this video] Tikhon Jelvis - Analyzing Programs with Z3 - [LINK] - Nadia Polykarpova on Z3 - SAT SMT school [LINK] - Emina Torlak's course [LINK] - Lindsey Kuper - SMT Solving and Solver-Aided Systems [LINK] - [LINK]