Compose Conference
2 HN recommenders · recommended in 3 months, 2016–2021
43:31 · 24K views · Jul 21, 2016
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 comments from Hacker News
### 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 the verification for yourself. Pact inlines at module creation/update time as a safety feature -- this way if a dep upgrades the code your contract runs doesn't change though the dep can revoke your code's right to access its tables/data until you update your contract. The "no leftpad" approach to deps. All the imported code that's pure, however, still works. This way, when you are building a module, you know that the code you formally verified/tested against is the only code that will ever run (until you update it). ### Whitepapers Thanks for the offer but I've already got enough people looking at them currently and we're keeping them confidential for now... a glaring stupid mistake would be embarrassing. Subscribe to the mailing list on kadena.io and you'll get updated with them the secon
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.
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]