Aeon programming language

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

SEARCH: Symmetric Encryption Algorithm Research

Learner-Verifier Framework for formal synthesis of Control Barrier Functions (CBF).

A fuzzing framework for SMT solvers

Infer Minimalist Grammars using the Z3 SMT-solver

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

This repository features AI-based game projects (Tic-tac-toe, Checkers, Sudoku solver) developed as part of the CS 235 course (optional).

MachSMT: An ML-Driven Algorithm Selection tool for SMT Solvers

A generator for Semantic Fusion

Implementation of LTSDiff algorithm

An efficient SMT solver that can solve pure boolean, UF and TQ formulas.

Given a simple VLSI (Very Large Scale Integration), use Constraint Programming, SAT and SMT solver, to provide the solution with the minimum height of the silicon chip

Python bindings for yices2

Intrepyd Model Checker

An experimental obfuscator for software protection using the SMT-based code generation

Angr CTFs covering topics from basics to intermediate.

A diabolic implementation of mcSAT 😈

The final project in the course "Automated reasoning about software" 67532 (The Hebrew University of Jerusalem).

Code and exercises for a workshop on z3 and angr