Programming in Z3 by learning to think like a compiler

This page summarizes the projects mentioned and recommended in the original post on news.ycombinator.com

Our great sponsors
  • Scout APM - Less time debugging, more time building
  • SonarLint - Deliver Cleaner and Safer Code - Right in Your IDE of Choice!
  • OPS - Build and Run Open Source Unikernels
  • GitHub repo alive2

    Automatic verification of LLVM optimizations

    Alive/Alive2 [1] is one of the most famous frameworks for compiler transformation verification using BitVec logic

    [1] https://github.com/AliveToolkit/alive2

  • GitHub repo recreational-rosette

    Some fun examples of solving problems with symbolic execution

    I don't know about "practical," but you might enjoy this: https://github.com/kach/recreational-rosette

  • Scout APM

    Less time debugging, more time building. Scout APM allows you to find and fix performance issues with no hassle. Now with error monitoring and external services monitoring, Scout is a developer's best friend when it comes to application development.

  • GitHub repo zz

    🍺🐙 ZetZ a zymbolic verifier and tranzpiler to bare metal C

    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.

    [0] https://github.com/zetzit/zz

  • GitHub repo taxoptimizer

    I used it to do some tax optimization around ISOs at a newly public company (https://gitlab.com/mbryant/taxoptimizer/-/blob/master/amt.py). It gets pretty slow when you try to look more than a few years out, so I'm guessing writing some optimization logic by hand would've made more sense. Using Z3 here definitely beat me trying to do this on paper like I've seen other people do!

  • GitHub repo angr

    A powerful and user-friendly binary analysis platform!

    angr uses z3.

    https://github.com/angr/angr

    Supposedly, the DoD has used angr for some use cases.

  • GitHub repo CrossHair

    An analysis tool for Python that blurs the line between testing and type systems.

    There's a tool for verification of Python programs based on contracts which uses Z3: https://github.com/pschanely/CrossHair

    You can use it as part of your CI or during the development (there's even a neat "watch" mode, akin to auto-correct).

NOTE: The number of mentions on this list indicates mentions on common posts plus user suggested alternatives. Hence, a higher number means a more popular project.

Suggest a related project

Related posts