z3-smt-solver
There are 53 repositories under z3-smt-solver topic.
sdasgup3/validating-binary-decompilation
Scalable Validator for Binary Lifters
codersguild/Software-Analysis-PAVT
Program Analysis, Software Verification & Testing. Python3, CAS, Dafny, Z3, CVC4, UCLID, ZChaff, NuSMV, AFL, Scala, CBMC & LLVM Framework (CO).
nickgildea/z3_codegen
A toy code generator (i.e. "program synthesis") using the Z3 solver
Brissouille/Lagrange
Cryptanalysis on differents algorithms with z3 solver sat
mistupv/SWIPrologZ3
A simple Prolog API for the Z3 constraint solver
umangm/realsyn
Automated Controller Synthesis
LuizZak/swift-z3
A Swift wrapper over Microsoft's Z3 Theorem Prover
OktaSecurityLabs/hack_url_re
Automatic hacking tool for URL regexes.
classicwuhao/qmaxuse
QMaxUSE: A query-based verification tool for verifying UML class diagrams with extreme size of OCL invariants.
DDiekmann/Applied-Verification-Lab-Neural-Networks
Some tutorials for different approaches to verify neural networks.
VictorAlonsoCM/CTFs
Here are some examples and solution of CTF Reverse Engineering and Pwning challenges where I have participated and solved using many tools such as Z3, Angr, IDA Pro and others software and tools.
xennygrimmato/z3-floating-point-proofs
Automated Proofs about floating-point numbers using Z3 Theorem Prover
jubitaneja/souper-cgo20-artifact
"Testing Static Analyses for Precision and Soundness". This is an artifact of our work accepted at the CGO 2020.
pncnmnp/Crossword-Solver
Mini crosswords solved quickly by guessing and positioning clues on the grid using Z3 SMT solver
nicolodon/MCVRP
Solving the MCVRP problem using: Constraint Programming, Satisfiability Module Theory and Mixed Integers Linear Programming.
VeriFIT/z3-noodler
The Z3-Noodler String Solver
notify-bibi/TriggerBug
本科毕设. Fast-Symbolic-Emulation-Engine. 因受够了 angr 诞生的项目，当年帮我solve了很多ctf题目嘻嘻，不过符号执行部分很少维护了，后面可能会用来做一些程序分析，反混淆也是不错. ( 暖心tips: 设置private再public会丢失star喔, 可惜我那为数不多的30几个star ... )
fredwangwang/webcam-sudoku-solver
A realtime webcam sudoku solver.
indurks/mgsmt
A parser for minimalist grammars that uses the Z3 SMT-solver.
SamTheMar/Strip_packing_problem
The strip packing problem is a 2-dimensional geometric minimization problem. Given a set of axis-aligned rectangles and a strip of bounded width and infinite height, determine an overlapping-free packing of the rectangles into the strip minimizing its height.
vietdoo/draw-groups-connected-shapes
This program is designed to tackle the challenge of grouping intersecting shapes and coloring them in a unified way. By using a set of algorithms and data structures, the program is able to efficiently identify overlapping areas between shapes and assign them to the same group.
AlexanderViand-Intel/z3-fhe-experiments
Experiments in using Z3 to check common FHE transformations
benbrastmckie/ModelChecker
A hyperintensional theorem prover for counterfactual conditional, modal, constitutive explanatory, relevance, and extensional operators.
Double-oxygeN/z3nim
Z3 Nim binding
rhalbersma/zed
Z3-Python scripts to solve N-queens type puzzles on a Stratego board
silab-nitkc/pukeko
An experimental LLVM-IR code fragment generator using the SMT solver Z3.
vkobel/z3-shamir-secret-sharing
Implementation of Shamir Secret Sharing using Z3
andreafra/piacere-model-checker
PIACERE DOML Model Checker
Erhtric/VLSI
This is the repo for the project in Combinatorial Decision Making and Optimization at @unibo.: solving a Very Large Scala Integration (VLSI) where we have to optimally fill a chip board by exploiting combinatorially the combinations using MiniZinc and Z3.
fmerizzi/VLSI_project
Combinatiorial Optimization applied to the rectangle packing problem, using Minizinc and Z3 solvers
indurks/mgsmt-inference
Infer Minimalist Grammars using the Z3 SMT-solver
lolloloschi97/Very-Large-Scale-Integration
Very Large Scale Integration solved using Costraint Programming and Minizinc
srapaport/Coop-robot
Algorithm using Interpolation to determine if a 'Robot move' strategy is efficient when the goal is to gather robots on one point
tensor-fusion/Einstein-Riddle-Z3
Solving Einstein's Fish riddle with the Z3 theorem prover.
WizzyGeek/z3sudoku
Solve sudoku puzzle with z3 theorem prover