Hacker news

  • Top
  • New
  • Past
  • Ask
  • Show
  • Jobs

Online Z3 Guide (https://microsoft.github.io)

71 points by Bluestein 5 days ago | 15 comments | View on ycombinator

olooney 3 days ago |

I 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-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.

greatgib 3 days ago |

If anyone wondering, because it took me a few hops to find out:

Z3 is a high-performance theorem prover being developed at Microsoft Research.

ascent817 3 days ago |

I’m working on a DO-178C compliant verification suite for avionics software with Z3 at work, criminally underrated