Scalable Validator for Binary Lifters

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

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

Cryptanalysis on differents algorithms with z3 solver sat

Automated Controller Synthesis

A simple Prolog API for the Z3 constraint solver

Automatic hacking tool for URL regexes.

A Swift wrapper over Microsoft's Z3 Theorem Prover

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

The Z3-Noodler String Solver

Some tutorials for different approaches to verify neural networks.

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.

A hyperintensional theorem prover for counterfactual conditional, modal, constitutive explanatory, relevance, and extensional operators.

Automated Proofs about floating-point numbers using Z3 Theorem Prover

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

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

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

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

Approximate Logic Synthesis via Iterative SMT-based Subcircuit Rewriting

A realtime webcam sudoku solver.