A bounded model checker for an IMP-style imperative language.
-
Updated
Feb 23, 2019 - Rust
A bounded model checker for an IMP-style imperative language.
Z3 backend for Fugue's concolic interpreter.
A symbolic executor for the QBE intermediate language
⚖️ A simple tool for calculating the optimal number of shares to buy to maintain a proportional portfolio
The axiom profiler for exploring and visualizing SMT solver quantifier instantiations (made via E-matching).
Add a description, image, and links to the z3 topic page so that developers can more easily learn about it.
To associate your repository with the z3 topic, visit your repo's landing page and select "manage topics."