Neos: Netlist encryption and obfuscation suite

This project is an object-oriented framework written in modern C++ for gate-level netlist obfuscation/deobfuscation. The tool contains a set of obfuscation and deobfuscation utilities and can be used through the command line.

Download

Z3: Z3 Theorem Prover

Z3 is a satisfiability modulo theories (SMT) solver developed by Microsoft. Z3 was developed in the Research in Software Engineering (RiSE) group at Microsoft Research Redmond and is targeted at solving problems that arise in software verification and program analysis. Z3 supports arithmetic, fixed-size bit-vectors, extensional arrays, datatypes, uninterpreted functions, and quantifiers. Its main applications are extended static checking, test case generation, and predicate abstraction.

Download

Gurobi Optimizer

Gurobi is used for linear programming (LP), quadratic programming (QP), quadratically constrained programming (QCP), mixed integer linear programming (MILP), mixed-integer quadratic programming (MIQP), and mixed-integer quadratically constrained programming (MIQCP).

Download