2 hours ago by remexre
I really like Z3 for showing that my weird bitwise hacks (e.g. [0]) are correct -- it's especially useful that I can show not only that a function is correct, but also that it approximates the correct answer to within whatever bounds I like. Plus, I can put it in a script, and shove it into the docs and tests easily. (Showing that the code actually corresponds to the Z3 equations needs symbolic execution, which I haven't set up yet though...)
[0]: https://doc.stahlos.com/kernel/notebooks/hashtables.html#est...
4 hours ago by iou
Nice article!!
I don't think it specifically states that this is z3-python (not a nitpick) which has an added bonus in that you can handle the SSA requirements if you're allocating inside a finite loop in the higher level language.
I was stuck on that at one time in the past, and then realized that not all the python code is in the scope of the solver and hence helps you automate those state additions.
These techniques aren't purely academic either, I've used them for reverse-engineering malware and software vulnerability analysis e.g. this inversion of MurmurHash3 https://www.josephkirwin.com/2018/04/07/z3-hash-inversions/
4 hours ago by iou
Oh and there's one other ridiculously cool feature that would go nicely with this blog post about "thinking like a compiler" and that's BitVec
Some info here https://www.josephkirwin.com/2017/11/16/constraint-solver-ti...
Essentially though, you can model fixed width integers signed/unsigned using that and make assertions on things like integer overflow or change in signed-ness.
Uwaterloo did some work to abstract Strings ontop of BitVec so you can include them in your solver state too, worth a look to people that like this content https://z3string.github.io/
3 hours ago by mshockwave
Alive/Alive2 [1] is one of the most famous frameworks for compiler transformation verification using BitVec logic
2 hours ago by Recursing
I wonder if there is a collection somewhere of practical uses of z3? (The simpler the better)
I have also used z3 to solve puzzles and toy problems, and found it magical, but can't seem to find any use case for it in practical problems :(
17 minutes ago by the-smug-one
It's more likely to be used by someone who then implements a practical tool on top of it. I used it to prove relational properties of WASM programs, which is useful to prove security properties like constant-time or differential privacy. You can also use it to prove program equivalence, which I think would be neat for testing a compiler with.
41 minutes ago by sigstoat
https://sat-smt.codes/ comes up on HN with some regularity, i think.
"practical uses" tends to mean whatever the speaker wants it to mean, so no guarantees, but i think it covers a number of small useful tasks, in addition to many of the common code golf type things.
an hour ago by csb6
Here [1] is a cool project that uses Z3 to make graphics specified by constraints.
I remember reading an article about someone using Z3 to optimize the placement of cutout drawings on a piece of paper (kind of like a spritesheet) and optimizing for the smallest possible area in order to reduce the use of paper/materials. However, I can't seem to find the article anywhere.
One more use of z3 is as one of the available solvers for a tool called gnatprove [2], which is used to prove/verify the correctness of programs written in the SPARK subset of the Ada programming language. SPARK is used to program safety-critical aeronautical/military projects.
[1] https://www.anishathalye.com/2019/12/12/constraint-based-gra...
[2] https://docs.adacore.com/spark2014-docs/html/ug/en/gnatprove...
an hour ago by fruffy
To explore Z3 projects, I sometimes just browse the tags on Github [0]. I also am not aware of a better way to get an overview. However, I know Z3 is used a lot in industry for verification and resource allocation tasks.
Personally, I have made extensive use of Z3 to find bugs in domain-specific language (DSL) compilers [1]. You can use Z3 to encode the source code before and after a compiler optimization as a logic formula and then check whether the formulae are equivalent. If they are not, there is likely a semantic bug in the transformation pass of your compiler, meaning you have introduced a subtle logic mistake.
This style of verification really works best if your programming language is sufficiently restricted (not Turing-complete) or if you pick isolated segments in your code (e.g., functions). If that is the case, these methods can be extremely effective. We have found many semantic bugs in a short time period. In our case, Z3 was not even the bottleneck, performance-wise. It was our language interpreter. And because the language is sufficiently restricted, we can even run our tool as part of the compiler CI. So whenever a pull request is made, we can check whether it may lead to subtle issues in program translation.
Another useful aspect of using Z3 to represent a programming language is that you can also generate test cases for your programs. As far as I know, the Rosette [2] framework is intended to make all of this more approachable.
[0]https://github.com/search?q=topic%3Az3&type=Repositories [1]https://www.usenix.org/conference/osdi20/presentation/ruffy [2]https://emina.github.io/rosette/
an hour ago by sweetsocks21
This post reminds me that I've been wanting to try out ZetZ[0]. It incorporates Z3 into a high-level programming language, and seems to do a lot of what the post talks about automatically.
Daily digest email
Get a daily email with the the top stories from Hacker News. No spam, unsubscribe at any time.