4 ms·
Online Z3 Guide
- greatgib 1mo agoIf anyone wondering, because it took me a few hops to find out: Z3 is a high-performance theorem prover being developed at Microsoft Research.
- Bluestein 1mo agoOr a BMW, or a groundbreaking electro mechanical computer, depending :)
- number6 1mo agoI was hoping for the mechanical computer...
- 112233 1mo agooh, something new! I thought Z3 is SAT/SMT solver, they must have added something.
- IshKebab 1mo agoIt is. Look up what SMT stands for.
- mcphage 1mo agoShin Megami Tensei?
- NooneAtAll3 1mo agoSMT is SAT+arithmetic, no?
- IshKebab 1mo agoSatisfiability Modulo Theories
- baq 1mo agowell a SAT solver is kinda sorta a theorem prover right...?
- Jaxan 1mo agoSometimes you can use SMT for “theorem proving”. It is a rather broad term. I don’t think they added something much different than what they already had.
- okokwhatever 1mo agonailed!
- olooney 1mo agoI like Z3 a lot. I think it's criminally underappreciated and underused. Here is a fairly interesting use I put it to a few years ago: https://www.oranlooney.com/post/playfair/#known-plaintext-attack https://www.oranlooney.com/post/playfair/#known-plaintext-at... Slightly more complicated than the toy examples shown in the documentation above, and hints at one of the real world use cases for Z3 - red teaming cryptography. That said, I'm not sure the documentation linked above is really doing it any favors in terms of helping popularizing it.
- lloydatkinson 1mo agoHow does it compare to the others? I started trying to use Zinc but I get lost in all the vocabulary and literature which assumes you already have a background in it.
- Bluestein 1mo agoThere's also a neat shm library by that name. Namespace's getting crowded :)
- ascent817 1mo agoI’m working on a DO-178C compliant verification suite for avionics software with Z3 at work, criminally underrated