Other Projects

MapleSAT

MapleSAT series of SAT solvers is a family of conflict-driven clause-learning SAT solvers outfitted with machine learning-based heuristics.

Z3 String Solver

Z3 String solver is a constraint solver for the quantifier-free theory of string equations, the regular-expression membership predicates, and linear arithmetic over the length functions. Z3 string solver is implemented as a string theory plug-in of the powerful Z3 SMT solver.

MapleCrypt

MapleCrypt line of research focuses on tailoring the internals of SAT solvers to cryptographic problems as well as applying machine learning for splitting heuristics in parallel SAT solvers.

MathCheck

MathCheck is a combination of the computer algebra system (CAS) SAGE with a SAT Solver. Users can define predicates in the language of the CAS which can be finitely verified in a loop by the SAT solver, analogous to basic SMT approaches.

Attack Resistant Security Defense Mechanims

Attack resistance is a formal approach aimed at analyzing security defense mechanisms (e.g., ASLR, ISR,…) and cryptographic obfuscation methods with the goal of ascertaining whether they are secure.