Scalable Validator for Binary Lifters
-
Updated
Jun 28, 2020 - LLVM
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
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
Mini crosswords solved quickly by guessing and positioning clues on the grid using Z3 SMT solver
"Testing Static Analyses for Precision and Soundness". This is an artifact of our work accepted at the CGO 2020.
Solving the MCVRP problem using: Constraint Programming, Satisfiability Module Theory and Mixed Integers Linear Programming.
A hyperintensional theorem prover for counterfactual conditional, modal, constitutive explanatory, relevance, and extensional operators.
本科毕设. Fast-Symbolic-Emulation-Engine. 因受够了 angr 诞生的项目,当年帮我solve了很多ctf题目嘻嘻,不过符号执行部分很少维护了,后面可能会用来做一些程序分析,反混淆也是不错. ( 暖心tips: 设置private再public会丢失star喔, 可惜我那为数不多的30几个star ... )
A realtime webcam sudoku solver.
Add a description, image, and links to the z3-smt-solver topic page so that developers can more easily learn about it.
To associate your repository with the z3-smt-solver topic, visit your repo's landing page and select "manage topics."