Coefficient-Based Reconstruction of Arithmetic — a Mixed Boolean-Arithmetic (MBA) expression simplifier for deobfuscation
Constraint solver based on coverage-guided fuzzing
Counter-example guided inductive synthesis (CEGIS) implementation for the SMT solver Z3 by Microsoft Research
A toy code generator (i.e. "program synthesis") using the Z3 solver
Sudoku Solver using Z3
Validate semantic equivalence between C++ and Rust LLVM IR using State-Of-The-Art Verification
A Swift wrapper over Microsoft's Z3 Theorem Prover
Mapping Quantum Circuits to IBM QX Architectures Using the Minimal Number of SWAP and H Operations
A reference implementation of PDR for boolean transition systems
Hoare logic for classroom demonstration
LLVM IR superoptimizer for HexCore — Z3 SMT-based synthesis engine for the Remill → Souper → Helix decompilation pipeline.
A Golang wrapper for the Z3 SMT solver
The Z3 Theorem Prover ~ Forked to enable automated Docker image builds and pushing to DockerHub 🚚
DepKit: A Typed Language for Advanced Package Management
Automated static builds of Z3 Theorem Prover for multiple platforms using GitHub Actions
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."