SAT, SMT and SAT+CAS solvers (actively supported)
- MathCheck: A SAT+CAS DPLL(CAS) verification tool for mathematical conjectures
- MapleSAT: An award-winning Boolean SAT solver that uses reinforcement-learning based branching
- Z3 string solver: An SMT constraint solver for string equations, regular expressions, and linear arithmetic
- StringFuzz: A random and mutation fuzzer for a theory of string equations, regular expressions, and linear arithmetic
- STP:
A constraint solver for bit-vectors and arrays. Important tools using STP
include KLEE, S2E, Souper, BAP and Java PathFinder
Automated Error
Finding Tools (not actively supported anymore)
- Mohawk: Automatic Error Finding in Access-Control Policies
- BuzzFuzz: A Dynamic Taint-based
Directed Fuzzing Tool
- jFuzz: A Concolic Whitebox Fuzzer for Java
Older Software Projects (not actively supported anymore)
- Hampi: A solver for string constraints
- SATGraf: A visualization and evolution tool for SAT solvers
- Lynx: A programmatic SAT solver (Uses a variation on the DPLL(T) idea)
- CVC Lite:
An SMT solver. I worked on the bit-vector and arrays theory solver in CVC Lite
- Mobile code security: A Java-based filtering and sanitization tool for mobile-code security
- Retargetable compilers: A compiler that can be easily retargeted via a declarative language to any processor
