benjamin051000/modpack-factory

SATisfying Minecraft modpack creator. 🏭

Language: Python - Size: 99.6 KB - Last synced at: 3 days ago - Pushed at: 3 days ago - Stars: 0 - Forks: 0

toolCHAINZ/jingle

SMT Modeling for Ghidra's PCODE

Language: Rust - Size: 339 KB - Last synced at: 3 days ago - Pushed at: 3 days ago - Stars: 26 - Forks: 5

se-buw/fm-playground

A Formal Method playground for limboole, Z3, nuXmv, Alloy, and Spectra

Language: TypeScript - Size: 104 MB - Last synced at: 4 days ago - Pushed at: 4 days ago - Stars: 12 - Forks: 2

mbeddr/mbeddr.formal

FASTEN: FormAl SpecificaTion ENvironment - a set of DSLs to experiment with rigorous systems and safety engineering.

Language: JetBrains MPS - Size: 178 MB - Last synced at: 4 days ago - Pushed at: 5 days ago - Stars: 27 - Forks: 15

astrofra/pLLuMdered-hearts

Language: Python - Size: 29.3 KB - Last synced at: 6 days ago - Pushed at: 6 days ago - Stars: 0 - Forks: 0

formalsec/smtml

An SMT solver frontend for OCaml

Language: OCaml - Size: 2.75 MB - Last synced at: 7 days ago - Pushed at: 7 days ago - Stars: 39 - Forks: 11

testsmt/yinyang

A fuzzing framework for SMT solvers

Language: Python - Size: 3.03 MB - Last synced at: 8 days ago - Pushed at: almost 2 years ago - Stars: 191 - Forks: 23

VeriFIT/z3-noodler Fork of Z3Prover/z3

The Z3-Noodler String Solver

Language: C++ - Size: 126 MB - Last synced at: about 9 hours ago - Pushed at: about 10 hours ago - Stars: 14 - Forks: 7

bliutech/mbased

MIT IEEE URTC 2024. GSET 2024. Repository for the "MBASED: Practical Simplifications of Mixed Boolean-Arithmetic Obfuscation". A Binary Ninja decompiler plugin taking ideas from compiler construction to simplify obfuscated boolean expressions.

Language: Python - Size: 873 KB - Last synced at: 4 days ago - Pushed at: 10 months ago - Stars: 13 - Forks: 1

pschanely/CrossHair

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

Language: Python - Size: 4.79 MB - Last synced at: 10 days ago - Pushed at: 10 days ago - Stars: 1,154 - Forks: 59

epfl-lara/stainless

Verification framework and tool for higher-order Scala programs

Language: Scala - Size: 139 MB - Last synced at: about 18 hours ago - Pushed at: 23 days ago - Stars: 375 - Forks: 56

trailofbits/manticore

Symbolic execution tool

Language: Python - Size: 43.5 MB - Last synced at: 17 days ago - Pushed at: over 1 year ago - Stars: 3,760 - Forks: 479

soaibsafi/smt-z3-vscode

VSCode extension for SMT2 language with Z3 solver

Language: TypeScript - Size: 593 KB - Last synced at: 26 days ago - Pushed at: 26 days ago - Stars: 0 - Forks: 0

bohlender/vim-smt2

A Vim plugin that adds support for the SMT-LIB2 format (including Z3's extensions)

Language: Vim Script - Size: 253 KB - Last synced at: about 1 month ago - Pushed at: about 1 month ago - Stars: 38 - Forks: 4

endjin/Z3.Linq

LINQ bindings for the Z3 theorem prover from Microsoft Research.

Language: C# - Size: 476 KB - Last synced at: about 1 month ago - Pushed at: 7 months ago - Stars: 38 - Forks: 3

obijywk/grilops

a GRId LOgic Puzzle Solver library

Language: Python - Size: 1.23 MB - Last synced at: about 1 month ago - Pushed at: over 1 year ago - Stars: 75 - Forks: 6

viperproject/smt-scope

SMTscope automatically analyses and visualises SMT solver execution traces.

Language: Rust - Size: 182 MB - Last synced at: 24 days ago - Pushed at: 3 months ago - Stars: 37 - Forks: 5

FSecureLABS/z3_and_angr_binary_analysis_workshop

Code and exercises for a workshop on z3 and angr

Language: Python - Size: 1.45 MB - Last synced at: 28 days ago - Pushed at: over 4 years ago - Stars: 227 - Forks: 39

deut-erium/auto-cryptanalysis

Automated cryptanalysis of substitution permutation network cipher

Language: Python - Size: 120 KB - Last synced at: 29 days ago - Pushed at: 9 months ago - Stars: 31 - Forks: 0

ThatNerdUKnow/dungeons-and-diagrams

TUI application using z3 to solve dungeons&diagrams puzzles

Language: Go - Size: 187 KB - Last synced at: 4 days ago - Pushed at: about 1 month ago - Stars: 0 - Forks: 0

mryndzionek/z3_schedule

Real time periodic task scheduling using Z3

Language: Python - Size: 356 KB - Last synced at: about 2 months ago - Pushed at: about 2 months ago - Stars: 0 - Forks: 0

ViRb3/z3-python-ctf

🐍 Solving CTF challenges using Z3 and Python

Language: Python - Size: 299 KB - Last synced at: about 2 months ago - Pushed at: almost 2 years ago - Stars: 60 - Forks: 4

mc-imperial/jfs

Constraint solver based on coverage-guided fuzzing

Language: C++ - Size: 1.64 MB - Last synced at: about 2 months ago - Pushed at: over 1 year ago - Stars: 244 - Forks: 20

nyu-systems/gauntlet

Finding bugs in P4 compilers using translation validation.

Language: P4 - Size: 23.6 MB - Last synced at: 2 months ago - Pushed at: 2 months ago - Stars: 37 - Forks: 3

Jakob-Bach/Solver-Demo

Demonstration of some MIP/SAT/SMT solvers/optimizers in multiple programming languages.

Language: Python - Size: 136 KB - Last synced at: 2 months ago - Pushed at: 2 months ago - Stars: 2 - Forks: 2

Indrajit-hub/ACAS-Xu-Verification-using-Z3

Language: Jupyter Notebook - Size: 220 KB - Last synced at: 2 months ago - Pushed at: 2 months ago - Stars: 0 - Forks: 0

Samuel-BlankAmber/linkedin-games-ai

Automatic solver for the five LinkedIn games: Tango, Queens, Pinpoint, Crossclimb, & Zip

Language: TypeScript - Size: 86.9 KB - Last synced at: 2 months ago - Pushed at: 2 months ago - Stars: 1 - Forks: 0

MusadiqPasha/FlowFree-Solver

This Python bot is an automated solver for the popular puzzle game Flow Free. Leveraging the power of the Z3 constraint solver, the bot intelligently solves Flow Free puzzles by strategically connecting matching-colored pipes without any user input.

Language: Python - Size: 23.4 MB - Last synced at: 2 months ago - Pushed at: 11 months ago - Stars: 5 - Forks: 0

nwad123/z3_recipes

My python script for recreating recipes using Z3.

Language: Python - Size: 7.81 KB - Last synced at: 8 days ago - Pushed at: 3 months ago - Stars: 0 - Forks: 0

LuizZak/swift-z3

A Swift wrapper over Microsoft's Z3 Theorem Prover

Language: C++ - Size: 117 MB - Last synced at: 2 months ago - Pushed at: 6 months ago - Stars: 12 - Forks: 5

OliverKovacs/find-circuit

Python code for finding circuits with a given truth table.

Language: Python - Size: 1.95 KB - Last synced at: 2 months ago - Pushed at: 3 months ago - Stars: 0 - Forks: 0

philzook58/z3_tutorial

Jupyter notebooks for tutorial on the Z3 SMT solver

Language: Jupyter Notebook - Size: 1.19 MB - Last synced at: about 1 month ago - Pushed at: over 1 year ago - Stars: 160 - Forks: 20

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.

Language: JavaScript - Size: 12 MB - Last synced at: about 1 month ago - Pushed at: 11 months ago - Stars: 20 - Forks: 4

IagoAbal/haskell-z3

Haskell bindings to Microsoft's Z3 API (unofficial).

Language: Haskell - Size: 824 KB - Last synced at: 11 days ago - Pushed at: over 1 year ago - Stars: 58 - Forks: 46

ahf/binarypuzzle

Python library for solving Binary Puzzles using Z3.

Language: Python - Size: 6.84 KB - Last synced at: 4 days ago - Pushed at: about 5 years ago - Stars: 2 - Forks: 1

ViRb3/z3-wasm 📦

Run Z3 entirely in your browser using WebAssembly

Language: JavaScript - Size: 14 MB - Last synced at: about 1 month ago - Pushed at: about 3 years ago - Stars: 7 - Forks: 4

PSS1998/MicroViper-Verifier

A deductive program verification tool for MicroViper programming language

Language: Rust - Size: 94.7 KB - Last synced at: 4 months ago - Pushed at: 4 months ago - Stars: 0 - Forks: 0

Slava0135/gobber

Go symbolic execution (Z3 SMT solver)

Language: Go - Size: 137 KB - Last synced at: 2 months ago - Pushed at: 5 months ago - Stars: 0 - Forks: 0

py-typedlogic/py-typedlogic

Logic plus python types

Language: Python - Size: 5.02 MB - Last synced at: 3 months ago - Pushed at: 3 months ago - Stars: 9 - Forks: 1

SwadicalRag/mistria-crop-rotator

A React-based web application for optimizing crop rotations in Fields of Mistria

Language: TypeScript - Size: 90.8 KB - Last synced at: 3 months ago - Pushed at: 5 months ago - Stars: 0 - Forks: 0

falk-hueffner/sematrope

Superoptimizer using the z3 SMT solver

Language: C++ - Size: 21.5 KB - Last synced at: 3 days ago - Pushed at: about 4 years ago - Stars: 17 - Forks: 1

kazemihabib/Vehicle-routing-problem-VRP

This project, also known as the Vehicle Routing Problem (VRP), addresses the Multiple Couriers Planning (MCP) problem using Constraint Programming (CP), Satisfiability Modulo Theories (SMT), and Mixed-Integer Linear Programming (MIP) to optimize courier routes efficiently.

Language: Python - Size: 1.48 MB - Last synced at: 2 months ago - Pushed at: 6 months ago - Stars: 0 - Forks: 0

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.

Size: 3.24 MB - Last synced at: 2 months ago - Pushed at: almost 6 years ago - Stars: 55 - Forks: 1

formalmethods/intrepid

Intrepyd Model Checker

Language: Python - Size: 147 MB - Last synced at: 17 days ago - Pushed at: over 3 years ago - Stars: 18 - Forks: 1

Isopod00/FO3_to_CoR_Translation

This project aims to translate First-Order 3-variable (FO3) predicate logic into the Calculus of Relations (CoR).

Language: Python - Size: 26.9 MB - Last synced at: about 2 months ago - Pushed at: 6 months ago - Stars: 1 - Forks: 0

rizinorg/rz-solver

ROP SMT-Solver using rizin analysis plugins

Size: 63.5 KB - Last synced at: 4 days ago - Pushed at: 7 months ago - Stars: 0 - Forks: 0

uwplse/Casper

A compiler for automatically re-targeting sequential Java code to Apache Spark.

Language: Java - Size: 5.1 MB - Last synced at: about 2 months ago - Pushed at: almost 2 years ago - Stars: 50 - Forks: 5

nmeum/qsym

A symbolic executor for the QBE intermediate language

Language: Rust - Size: 107 KB - Last synced at: about 2 months ago - Pushed at: about 2 years ago - Stars: 1 - Forks: 0

darkmacheken/ALC 📦

Algorithms for Computational Logic's project.

Language: Python - Size: 16.9 MB - Last synced at: 10 months ago - Pushed at: over 5 years ago - Stars: 0 - Forks: 0

div72/valve

A WIP static analyzer for V.

Language: V - Size: 63.5 KB - Last synced at: about 2 months ago - Pushed at: over 2 years ago - Stars: 1 - Forks: 0

ykahalan/go-stp

Golang bindings to the STP API

Language: Go - Size: 4.88 KB - Last synced at: 3 months ago - Pushed at: over 3 years ago - Stars: 0 - Forks: 0

Dashstrom/z3-armor

Constraint-based obfuscation using z3.

Language: Python - Size: 2.7 MB - Last synced at: 11 days ago - Pushed at: 11 months ago - Stars: 1 - Forks: 0

tensor-fusion/Einstein-Riddle-Z3

Solving Einstein's Fish riddle with the Z3 theorem prover.

Language: SMT - Size: 8.79 KB - Last synced at: 3 months ago - Pushed at: about 1 year ago - Stars: 1 - Forks: 0

bunji2/practiceofdsl

Practice of DSL (described in Japanese)

Language: Go - Size: 1.24 MB - Last synced at: about 2 months ago - Pushed at: about 5 years ago - Stars: 1 - Forks: 0

paytonshafer/CS458-Formal-Methods-for-Program-Verification

CS458 at Clarkson University Spring 24

Language: SMT - Size: 383 KB - Last synced at: about 1 year ago - Pushed at: about 1 year ago - Stars: 0 - Forks: 0

danielbal21/BMC_Path_Planning

Solve grid-based pathfinding challenges efficiently. Our tool transforms grids into SAT problems using Kripke Structures and Boolean formulas, ensuring step-by-step validity while avoiding collisions. Simplify navigation in dynamic environments with central and dynamic agents.

Language: Python - Size: 54.6 MB - Last synced at: about 1 year ago - Pushed at: about 1 year ago - Stars: 0 - Forks: 0

dee-me-tree-or-love/z3 Fork of Z3Prover/z3

The Z3 Theorem Prover ~ Forked to enable automated Docker image builds and pushing to DockerHub :truck:

Language: C++ - Size: 112 MB - Last synced at: about 1 year ago - Pushed at: over 3 years ago - Stars: 1 - Forks: 0

kapaw/pwnmachine

Vagrant setup for building a machine for CTF/exploit development

Size: 40 KB - Last synced at: 7 months ago - Pushed at: about 6 years ago - Stars: 23 - Forks: 7

agilot/satapps

Scala library for solving NP-hard probems

Language: Scala - Size: 14.2 MB - Last synced at: about 1 year ago - Pushed at: over 1 year ago - Stars: 9 - Forks: 0

wadoon/mima-symbex

Symbolical Execution for MiniMal Assembler

Language: Python - Size: 3.91 KB - Last synced at: about 1 year ago - Pushed at: over 2 years ago - Stars: 0 - Forks: 0

kristinak228/Z3_Mutilated_Squares

Language: C++ - Size: 62.5 KB - Last synced at: about 1 year ago - Pushed at: over 7 years ago - Stars: 0 - Forks: 0

Patryk27/nonogram-solver

Solves monochromatic nonograms, powered by Rust and Z3

Language: Rust - Size: 4.88 KB - Last synced at: 3 days ago - Pushed at: about 1 year ago - Stars: 0 - Forks: 0

AlexanderViand-Intel/z3-fhe-experiments

Experiments in using Z3 to check common FHE transformations

Language: Python - Size: 10.7 KB - Last synced at: about 1 year ago - Pushed at: about 1 year ago - Stars: 1 - Forks: 1

kevinychen/nikoli-puzzle-solver

Solver for over 100 types of Nikoli-style logic puzzles

Language: TypeScript - Size: 4.06 MB - Last synced at: about 1 year ago - Pushed at: over 1 year ago - Stars: 19 - Forks: 1

Scheggetta/vehicle-routing-problem Fork of NglQ/vehicle-routing-problem

Multiple combinatorial optimization techniques applied to the VRP problem

Size: 1.54 MB - Last synced at: over 1 year ago - Pushed at: over 1 year ago - Stars: 0 - Forks: 0

rohitdureja/SimplePDR

A reference implementation of PDR for boolean transition systems

Language: C++ - Size: 8.02 MB - Last synced at: about 1 year ago - Pushed at: over 8 years ago - Stars: 8 - Forks: 2

markusbrammer/z3-dotnet

My attempt at understanding the Z3 API for .NET (F#)

Size: 7.81 KB - Last synced at: 3 months ago - Pushed at: about 1 year ago - Stars: 0 - Forks: 0

filipeom/queries

SMT Query Dataset

Size: 4.27 MB - Last synced at: 20 days ago - Pushed at: over 1 year ago - Stars: 0 - Forks: 0

scriptographers/CS228-Assignment-1

Assignment 1, Logic for Computer Science, Spring 2021, IIT Bombay

Language: Python - Size: 23.4 KB - Last synced at: over 1 year ago - Pushed at: over 4 years ago - Stars: 0 - Forks: 0

bramvdbogaerde/z3-wasm 📦

Scripts and Javascript Glue code to use Z3 in the browser using WASM

Language: JavaScript - Size: 32.2 KB - Last synced at: about 1 year ago - Pushed at: over 3 years ago - Stars: 13 - Forks: 7

philzook58/z3-rise4fun Fork of bramvdbogaerde/z3-wasm

Z3 tutorials from the rise4fun website

Language: JavaScript - Size: 11.4 MB - Last synced at: about 1 year ago - Pushed at: almost 3 years ago - Stars: 9 - Forks: 3

codersguild/simplr

A simple programming language for program verification using Z3, ANTLR4 & Parser Combinators written using Scala

Language: Java - Size: 14.8 MB - Last synced at: 6 days ago - Pushed at: over 4 years ago - Stars: 1 - Forks: 1

marcelwa/CEGIS

Counter-example guided inductive synthesis (CEGIS) implementation for the SMT solver Z3 by Microsoft Research

Language: C++ - Size: 15.6 KB - Last synced at: about 1 year ago - Pushed at: over 8 years ago - Stars: 43 - Forks: 6

lhengi/z3flowfreeSolver

Solution finder for a popular mobile game "Flow Free". Solution for this game is in NP-Complete. Derived a polynomial time reduction algorithm to reduce the problem to satisfiability problem.

Language: Python - Size: 41.7 MB - Last synced at: over 1 year ago - Pushed at: over 6 years ago - Stars: 1 - Forks: 1

sim642/z3em

Z3 via emscripten

Language: Shell - Size: 17.8 MB - Last synced at: 11 days ago - Pushed at: over 5 years ago - Stars: 8 - Forks: 1

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.

Language: Jupyter Notebook - Size: 8.67 MB - Last synced at: over 1 year ago - Pushed at: almost 3 years ago - Stars: 2 - Forks: 2

guyez/Present-Wrapping-Problem

CP and SMT model to solve the Present Wrapping Problem (PWP): given a wrapping paper roll of a certain dimen- sion and a list of presents, decide how to cut off pieces of paper so that all the presents can be wrapped. Consider that each present is described by the dimensions of the piece of paper needed to wrap it. Moreover, each necessary piece of paper cannot be rotated when cutting off, to respect the direction of the patterns in the paper.

Language: Python - Size: 196 KB - Last synced at: 5 months ago - Pushed at: almost 5 years ago - Stars: 1 - Forks: 0

usrl-uofsc/dji_gimbal_cam

A clean and simple package for use with DJI Gimballed Cameras

Language: C++ - Size: 40 KB - Last synced at: over 1 year ago - Pushed at: about 4 years ago - Stars: 4 - Forks: 2

Kiarahmani/CLOTHO

Directed Test Generation for Weakly Consistent Database Systems

Language: Java - Size: 31.6 MB - Last synced at: over 1 year ago - Pushed at: over 2 years ago - Stars: 3 - Forks: 4

ppmx/sudoku-solver

Sudoku Solver using Z3

Language: C++ - Size: 90.8 KB - Last synced at: over 1 year ago - Pushed at: over 5 years ago - Stars: 18 - Forks: 7

geoff-m/smtsudoku

Example usage of Z3 to solve sudoku

Language: C# - Size: 6.84 KB - Last synced at: over 1 year ago - Pushed at: over 1 year ago - Stars: 0 - Forks: 0

balajibalasubramaniam/dig

Size: 36 MB - Last synced at: over 1 year ago - Pushed at: over 7 years ago - Stars: 0 - Forks: 0

mwarzynski/uw_universality

Computing universality of Finite-State Automata using z3 solver.

Language: Python - Size: 6.84 KB - Last synced at: almost 2 years ago - Pushed at: about 6 years ago - Stars: 0 - Forks: 0

mwarzynski/uw_cargoes

Cargo puzzle SMT solver.

Language: Python - Size: 43 KB - Last synced at: almost 2 years ago - Pushed at: about 6 years ago - Stars: 0 - Forks: 0

jubitaneja/souper-cgo20-artifact

"Testing Static Analyses for Precision and Soundness". This is an artifact of our work accepted at the CGO 2020.

Language: C - Size: 171 MB - Last synced at: over 1 year ago - Pushed at: over 5 years ago - Stars: 6 - Forks: 0

zensum/leia

Leia writes HTTP requests to kafka topics, redis pub/sub or gcloud pub/sub.

Language: Kotlin - Size: 469 KB - Last synced at: almost 2 years ago - Pushed at: over 5 years ago - Stars: 5 - Forks: 2

zensum/katie 📦

Language: Kotlin - Size: 2.74 MB - Last synced at: almost 2 years ago - Pushed at: over 5 years ago - Stars: 1 - Forks: 1

zensum/franz 📦

A Kotlin library for running workers on Kafka

Language: Kotlin - Size: 271 KB - Last synced at: almost 2 years ago - Pushed at: over 5 years ago - Stars: 6 - Forks: 0

bcongdon/optimal_balancer

⚖️ A simple tool for calculating the optimal number of shares to buy to maintain a proportional portfolio

Language: Rust - Size: 48.8 KB - Last synced at: 3 months ago - Pushed at: almost 2 years ago - Stars: 2 - Forks: 1

arey0pushpa/pyZ3

Encoding Vesicle Traffic System in Z3 and CBMC

Language: TeX - Size: 13 MB - Last synced at: almost 2 years ago - Pushed at: over 5 years ago - Stars: 1 - Forks: 1

shraiysh/hoare-logic

Hoare logic for classroom demonstration

Language: C++ - Size: 50.8 KB - Last synced at: almost 2 years ago - Pushed at: over 5 years ago - Stars: 3 - Forks: 2

ciao-lang/ciao_z3

Z3 interface for Ciao

Language: SMT - Size: 20.5 KB - Last synced at: almost 2 years ago - Pushed at: over 5 years ago - Stars: 0 - Forks: 0

blukat29/regex-crossword-solver

https://regexcrossword.com/ solver using Z3py

Language: Python - Size: 37.1 KB - Last synced at: about 1 year ago - Pushed at: over 3 years ago - Stars: 17 - Forks: 4

Jmeyer1292/block_diagram_z3

Analyze and test safety programs written in the function block diagram language for Siemens' Fail-Safe PLCs with the Z3 SMT solver.

Language: Python - Size: 1.07 MB - Last synced at: about 1 year ago - Pushed at: over 3 years ago - Stars: 6 - Forks: 3

porglezomp/hyalite

A bounded model checker for an IMP-style imperative language.

Language: Rust - Size: 10.7 KB - Last synced at: 2 months ago - Pushed at: over 6 years ago - Stars: 7 - Forks: 0

lvijay/minesweeper-solver

An automated Minesweeper Solver

Language: Python - Size: 1.22 MB - Last synced at: almost 2 years ago - Pushed at: almost 2 years ago - Stars: 1 - Forks: 0

ACassimiro/TSNsched

Automated Schedule Generation for Time-Sensitive Networks (TSN).

Language: Java - Size: 260 MB - Last synced at: almost 2 years ago - Pushed at: almost 2 years ago - Stars: 69 - Forks: 29

aionescu/uu-mpsv-gcl-verifier

GCL verification tool based on predicate transformers

Language: Haskell - Size: 729 KB - Last synced at: 2 months ago - Pushed at: over 2 years ago - Stars: 2 - Forks: 0

enricomors/cdmo_vlsi

Repo for the project of the course on Combinatorial Decision Making and Optimization @ Unibo

Language: Jupyter Notebook - Size: 29.9 MB - Last synced at: 11 months ago - Pushed at: almost 2 years ago - Stars: 0 - Forks: 1

mistupv/SWIPrologZ3

A simple Prolog API for the Z3 constraint solver

Language: C - Size: 13.7 KB - Last synced at: about 1 year ago - Pushed at: over 7 years ago - Stars: 14 - Forks: 2