Roberto Paleari (@rpaleari)

Lorenzo Martignoni (@martignlo)

http://security.dico.unimi.it/~roberto/pystp/

STP

PySTP is a Python extension module that interfaces with STP. STP is a decision procedure for the theory of fixed-width bitvectors and arrays, and PySTP enables Python scripts to use STP.

???

???

Sascha Böhme

http://www4.in.tum.de/~boehmes/z3-python.html

Z3

This is a Python binding to the SMT solver Z3. Since it is based on Python's dynamic foreign function interface ctypes, no compilation is required. Z3 is a high-performance theorem prover being developed at Microsoft Research. Z3 supports linear real and integer arithmetic, fixed-size bit-vectors, extensional arrays, uninterpreted functions, and quantifiers. Z3 is integrated with a number of program analysis, testing, and verification tools from Microsoft Research. These include: Spec#/Boogie, Pex, Yogi, Vigilante, SLAM, F7, SAGE, VS3, FORMULA, and HAVOC. It can read problems in SMT-LIB and Simplify formats.

???

site Z3

Microsoft Research

http://research.microsoft.com/en-us/um/redmond/projects/z3/

Z3

Python interface for Z3. It covers all main features in the Z3 API. Z3 is a high-performance theorem prover being developed at Microsoft Research.

SEA
BARF
look_for_gadgets_with_equations.py
rop_compiler

guide