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.

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.

Automated Proofs about floating-point numbers using Z3 Theorem Prover

The Z3-Noodler String Solver

"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

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

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

本科毕设. Fast-Symbolic-Emulation-Engine. 因受够了 angr 诞生的项目，当年帮我solve了很多ctf题目，不过很少维护了，后面可能会用来做一些其他的程序分析，反混淆也是不错. ( 暖心tips: 设置private再public会丢失star喔, 可惜原来那为数不多的30几个star ... )

A realtime webcam sudoku solver.