sethirus/The-Thiele-Machine

A self-verifying proof that the Thiele Machine is a universal model of computation which strictly contains the Turing Machine as a blind, special case. All open source because no one has convinced me not to.

Language: Python - Size: 1.88 MB - Last synced at: 5 days ago - Pushed at: 5 days ago - Stars: 3 - Forks: 0

ChaariMahmoud/VeriSol-Extended

VeriSol Extended is an enhanced version of the original Microsoft Verisol with additional support for WebAssembly (WASM) smart contracts and modern .NET 9.0 framework.

Language: C# - Size: 21.8 MB - Last synced at: 16 days ago - Pushed at: 16 days ago - Stars: 0 - Forks: 0

benbrastmckie/ModelChecker

A hyperintensional theorem prover for rapidly prototyping modular semantic theories

Language: Python - Size: 15.6 MB - Last synced at: 19 days ago - Pushed at: 19 days ago - Stars: 7 - Forks: 2

VeriFIT/z3-noodler Fork of Z3Prover/z3

The Z3-Noodler String Solver

Language: C++ - Size: 129 MB - Last synced at: 22 days ago - Pushed at: 22 days ago - Stars: 16 - Forks: 8

LP-RG/subxpat

The SubXPAT approximate logic synthesis framework

Language: Python - Size: 24.7 MB - Last synced at: 8 days ago - Pushed at: 8 days ago - Stars: 7 - Forks: 0

matthewoestreich/js-randomness-predictor

Predict Math.random output in Node, Chrome, Firefox, and Safari

Language: TypeScript - Size: 337 KB - Last synced at: 25 days ago - Pushed at: about 1 month ago - Stars: 2 - Forks: 0

matthewoestreich/z3-static-build

Automated static builds of Z3 Theorem Prover for multiple platforms using GitHub Actions

Language: C++ - Size: 6.17 MB - Last synced at: about 2 months ago - Pushed at: about 2 months ago - Stars: 0 - Forks: 0

ConfirmedDev/Tyler-Ai-Logic-Solver-SAT-SMT-Dashboard

This project was designed to serve as a research-grade symbolic reasoning dashboard that helps others explore the bridge between computational logic and interactive visualization.

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

sschr15/kotlin-z3-wrapper

A way to interact with Z3 from Kotlin Multiplatform

Language: Kotlin - Size: 509 KB - Last synced at: 9 days ago - Pushed at: about 2 months ago - Stars: 0 - Forks: 0

jurisgpt/GrizlyUDVacator-CaseIntake

Symbolic AI for Legal Due Process – A domain-specific reasoning engine for Unlawful Detainer (Eviction) case triage, focused on default judgment relief under California CCP §§473(b) and 473.5. Unlike generative AI, this system performs formal legal reasoning using Answer Set Programming (Clingo), ensuring mathematically provable/ auditable o/p.

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

LilymoonW/FinalProject_CS340

This was created as part of our final project for Wellesley CS 340 project. Follows a interactive story where players navigate through a series of word logic puzzles. We model the word puzzles through formal verification tools Z3 and Alloy. Our aim is to formally encode each puzzle’s constraints, verify solution correctness with solvers.

Language: HTML - Size: 71.8 MB - Last synced at: about 1 month ago - Pushed at: 4 months ago - Stars: 1 - Forks: 0

AlexanderViand/z3-fhe-experiments

Experiments in using Z3 to check common FHE transformations

Language: Python - Size: 10.7 KB - Last synced at: 3 months ago - Pushed at: over 1 year ago - Stars: 2 - Forks: 0

teobanu21/SEARCH

SEARCH: Symmetric Encryption Algorithm Research

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

sdasgup3/validating-binary-decompilation

Scalable Validator for Binary Lifters

Language: LLVM - Size: 1.01 GB - Last synced at: 5 months ago - Pushed at: about 5 years ago - Stars: 56 - Forks: 8

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

Language: Jupyter Notebook - Size: 220 KB - Last synced at: 5 months ago - Pushed at: 5 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: 5 months ago - Pushed at: 9 months ago - Stars: 12 - Forks: 5

notify-bibi/TriggerBug

Fast-Symbolic-Emulation-Engine. 主要用于自动化逆向约束求解，目的是解决angr的各种不足之处，大学时使用本工具solve了很多ctf题目，毕业后不打ctf了，很少维护了，后面可能会用来做一些其他的程序分析，反混淆也是不错. ( tips: repo设置private再public会丢失全部star, 原本还有30几个的 ... )

Language: C - Size: 109 MB - Last synced at: 7 months ago - Pushed at: 7 months ago - Stars: 6 - Forks: 1

DDiekmann/Applied-Verification-Lab-Neural-Networks

Some tutorials for different approaches to verify neural networks.

Language: Jupyter Notebook - Size: 3.97 MB - Last synced at: 7 months ago - Pushed at: almost 3 years ago - Stars: 10 - Forks: 4

adithyaov/general-scheduler

Language: Python - Size: 13.2 MB - Last synced at: 4 months ago - Pushed at: over 7 years ago - Stars: 3 - Forks: 0

immkg/general-scheduler

Timetable scheduling is a complex and challenging problem, especially in educational institutions where multiple constraints must be balanced

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

ykahalan/go-stp

Golang bindings to the STP API

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

codersguild/Software-Analysis-PAVT

Program Analysis, Software Verification & Testing. Python3, CAS, Dafny, Z3, CVC4, UCLID, ZChaff, NuSMV, AFL, Scala, CBMC & LLVM Framework (CO).

Language: Boogie - Size: 21.9 MB - Last synced at: 5 months ago - Pushed at: over 2 years ago - Stars: 37 - Forks: 6

salarkalan/Specs-Analysis

Analysis of Formal Specifications SAT, SMT, Alloy, NuSMV.

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

rhalbersma/zed

Z3-Python scripts to solve N-queens type puzzles on a Stratego board

Language: Python - Size: 65.4 KB - Last synced at: over 1 year ago - Pushed at: about 2 years ago - Stars: 2 - 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: 6 months ago - Pushed at: over 1 year ago - Stars: 1 - Forks: 0

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.

Language: C++ - Size: 32.2 MB - Last synced at: 5 months ago - Pushed at: over 2 years ago - Stars: 3 - Forks: 0

0cherry/miasm Fork of cea-sec/miasm

Reverse engineering framework in Python

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

Brissouille/Lagrange

Cryptanalysis on differents algorithms with z3 solver sat

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

markusbrammer/z3-dotnet

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

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

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

Language: Python - Size: 10.7 MB - Last synced at: over 1 year ago - Pushed at: over 2 years ago - Stars: 1 - Forks: 0

silab-nitkc/pukeko

An experimental LLVM-IR code fragment generator using the SMT solver Z3.

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

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: almost 2 years ago - Pushed at: about 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: 8 months ago - Pushed at: about 5 years ago - Stars: 1 - Forks: 0

nicolodon/MCVRP

Solving the MCVRP problem using: Constraint Programming, Satisfiability Module Theory and Mixed Integers Linear Programming.

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

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

indurks/mgsmt-inference

Infer Minimalist Grammars using the Z3 SMT-solver

Language: Python - Size: 1.03 MB - Last synced at: about 2 years ago - Pushed at: about 2 years ago - Stars: 0 - Forks: 0

indurks/mgsmt

A parser for minimalist grammars that uses the Z3 SMT-solver.

Language: Python - Size: 1.09 MB - Last synced at: about 2 years ago - Pushed at: about 2 years ago - Stars: 0 - Forks: 0

xennygrimmato/z3-floating-point-proofs

Automated Proofs about floating-point numbers using Z3 Theorem Prover

Language: Python - Size: 5.86 KB - Last synced at: 4 days ago - Pushed at: over 7 years ago - Stars: 7 - Forks: 2

pncnmnp/Crossword-Solver

Mini crosswords solved quickly by guessing and positioning clues on the grid using Z3 SMT solver

Language: Python - Size: 44.6 MB - Last synced at: about 1 month ago - Pushed at: about 1 year ago - Stars: 6 - Forks: 3

mistupv/SWIPrologZ3

A simple Prolog API for the Z3 constraint solver

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

cryhot/factosynth

A circuit network synthesizer for Factorio.

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

WizzyGeek/z3sudoku

Solve sudoku puzzle with z3 theorem prover

Language: Python - Size: 1000 Bytes - Last synced at: over 2 years ago - Pushed at: over 2 years ago - Stars: 1 - Forks: 0

umangm/realsyn

Automated Controller Synthesis

Language: Python - Size: 1.55 MB - Last synced at: over 2 years ago - Pushed at: about 7 years ago - Stars: 13 - Forks: 5

classicwuhao/qmaxuse

QMaxUSE: A query-based verification tool for verifying UML class diagrams with extreme size of OCL invariants.

Language: SMT - Size: 268 MB - Last synced at: over 2 years ago - Pushed at: almost 3 years ago - Stars: 7 - Forks: 1

OktaSecurityLabs/hack_url_re

Automatic hacking tool for URL regexes.

Language: Python - Size: 42 KB - Last synced at: over 2 years ago - Pushed at: over 4 years ago - Stars: 9 - Forks: 3

murumura/SAT-Problem

Solving Latin-Square & Sudoku problem by Z3-Solver and Qiskit-Solver

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

Double-oxygeN/z3nim

Z3 Nim binding

Language: Nim - Size: 84 KB - Last synced at: 5 months ago - Pushed at: over 5 years ago - Stars: 2 - Forks: 0

nickgildea/z3_codegen

A toy code generator (i.e. "program synthesis") using the Z3 solver

Language: C++ - Size: 11.7 KB - Last synced at: over 2 years ago - Pushed at: almost 8 years ago - Stars: 26 - Forks: 6

andreafra/piacere-model-checker Fork of michiari/piacere-mc-openapi

PIACERE DOML Model Checker

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

fredwangwang/webcam-sudoku-solver

A realtime webcam sudoku solver.

Language: Python - Size: 1.3 MB - Last synced at: 3 months ago - Pushed at: almost 4 years ago - Stars: 3 - Forks: 0

Erhtric/VLSI Fork of WenXiaowei/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.

Size: 8.7 MB - Last synced at: over 2 years ago - Pushed at: about 4 years ago - Stars: 1 - Forks: 0

fmerizzi/VLSI_project

Combinatiorial Optimization applied to the rectangle packing problem, using Minizinc and Z3 solvers

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

jstanley0/advent-2018

advent of code 2018 (most problems done with languages I am *not* proficient with, as a learning experience)

Language: Rust - Size: 53.7 KB - Last synced at: about 2 months ago - Pushed at: over 1 year ago - Stars: 0 - Forks: 0

neuschaefer/sudoku

Python sudoku tools based on the z3 solver

Language: Python - Size: 13.7 KB - Last synced at: over 2 years ago - Pushed at: over 3 years ago - Stars: 0 - Forks: 0

vkobel/z3-shamir-secret-sharing

Implementation of Shamir Secret Sharing using Z3

Language: Jupyter Notebook - Size: 7.81 KB - Last synced at: 5 months ago - Pushed at: over 6 years ago - Stars: 2 - Forks: 1

Enescigdem/Z3Solver_examples

Language: Python - Size: 14.6 KB - Last synced at: over 2 years ago - Pushed at: about 5 years ago - Stars: 0 - Forks: 0

EmreOzkose/solving-satisfaction-problems-with-theorem-provers

solving-satisfaction-problems-with-theorem-provers

Language: Python - Size: 28.3 KB - Last synced at: over 2 years ago - Pushed at: about 5 years ago - Stars: 0 - Forks: 0

greninja/CNF-Gen

Language: Python - Size: 472 KB - Last synced at: over 2 years ago - Pushed at: over 5 years ago - Stars: 1 - Forks: 0

SecurityArtWork/z3prover

Post related code

Language: Python - Size: 2.93 KB - Last synced at: about 1 month ago - Pushed at: about 8 years ago - Stars: 0 - Forks: 0