z3
There are 182 repositories under z3 topic.
trailofbits/manticore
Symbolic execution tool
pschanely/CrossHair
An analysis tool for Python that blurs the line between testing and type systems.
epfl-lara/stainless
Verification framework and tool for higher-order Scala programs
mc-imperial/jfs
Constraint solver based on coverage-guided fuzzing
FSecureLABS/z3_and_angr_binary_analysis_workshop
Code and exercises for a workshop on z3 and angr
kokjo/universalrop
Small tool for generating ropchains using unicorn and z3
testsmt/yinyang
A fuzzing framework for SMT solvers
philzook58/z3_tutorial
Jupyter notebooks for tutorial on the Z3 SMT solver
RocketRace/easy_z3
Using z3's never been easier (maybe)
ACassimiro/TSNsched
Automated Schedule Generation for Time-Sensitive Networks (TSN).
obijywk/grilops
a GRId LOgic Puzzle Solver library
IagoAbal/haskell-z3
Haskell bindings to Microsoft's Z3 API (unofficial).
SatyendraBanjare/plt-formal-methods-resources
Curated List of Research Focused Reading Materials & Videos for Learning about Programming Language Theory Research, Formal Methods and their application in some most active computer Science fields.
ViRb3/z3-python-ctf
🐍 Solving CTF challenges using Z3 and Python
marcelwa/CEGIS
Counter-example guided inductive synthesis (CEGIS) implementation for the SMT solver Z3 by Microsoft Research
uwplse/Casper
A compiler for automatically re-targeting sequential Java code to Apache Spark.
formalsec/smtml
An SMT solver frontend for OCaml
vmunoz82/eda_tools
A Dockerfile with a collections of ready to use open source EDA tools: Yosys, SimbiYosys (with Z3, boolector and Yices2), nextpnr-ice40, netxpnr-ecp5, nextpnr-gowin, Amaranth HDL, Silice and Verilator.
bohlender/vim-smt2
A Vim plugin that adds support for the SMT-LIB2 format (including Z3's extensions)
endjin/Z3.Linq
LINQ bindings for the Z3 theorem prover from Microsoft Research.
nyu-systems/gauntlet
Finding bugs in P4 compilers using translation validation.
nickgildea/z3_codegen
A toy code generator (i.e. "program synthesis") using the Z3 solver
termite-analyser/z3overlay
An overlay for the OCaml Z3 binding.
viperproject/smt-scope
SMTscope automatically analyses and visualises SMT solver execution traces.
deut-erium/auto-cryptanalysis
Automated cryptanalysis of substitution permutation network cipher
kevinychen/nikoli-puzzle-solver
Solver for over 100 types of Nikoli-style logic puzzles
toolCHAINZ/jingle
SMT Modeling for Ghidra's PCODE
mbeddr/mbeddr.formal
FASTEN: FormAl SpecificaTion ENvironment - a set of DSLs to experiment with rigorous systems and safety engineering.
philnguyen/z3-rkt
Racket bindings for Z3
zv/z3-mode
An interactive development environment for SMT-LIB files and Z3
kapaw/pwnmachine
Vagrant setup for building a machine for CTF/exploit development
frizensami/nus-timetable-optimizer
Codebase for the NUS Timetable Optimizer, a tool to help students at the National University of Singapore optimize their timetables to their liking.
blukat29/regex-crossword-solver
https://regexcrossword.com/ solver using Z3py
formalmethods/intrepid
Intrepyd Model Checker
ppmx/sudoku-solver
Sudoku Solver using Z3
saruman9/move_ctf_writeup
Writeup for Move CTF 2022 by MoveBit and others.