Anthony Desnos (@adesnos)

http://code.google.com/p/androguard/

Description : Androguard is mainly a tool written in python to play with Android :
- Dex (Dalvik virtual machine) (.dex), and ODex (disassemble, decompilation),
- APK (Android application) (.apk),
- Android's binary xml (.xml).

???

Documentation

Mario Vilas (@Mario_Vilas)

http://pypi.python.org/pypi/BeaEnginePython/

BeaEngine (http://www.beaengine.org/)

BeaEngine disassembler bindings for Python.

RopMount

Installers for BeaEnginePython, Pymsasid and PyDasm

Craig Heffnerf

https://code.google.com/p/binwalk/

Binwalk is a firmware analysis tool designed to assist in the analysis, extraction, and reverse engineering of firmware images and other binary blobs. It is simple to use, fully scriptable, and can be easily extended via custom signatures, extraction rules, and plugin modules.

???

Scripting with the Python API

Ero Carrera (@erocarrera)

https://github.com/zynamics/bochs-python-instrumentation

Bochs (2.4.5 and 2.4.6)

This patch for Bochs provides a Python interpreter instead of Bochs' own debugger, yet still providing the debugger functionality. It also allows to interact with the instrumentation interface on-demand, by dynamically associating Python methods to handle instrumentation events.

???

wiki
presentation

Grugq (@thegrugq)

https://github.com/grugq/Buggery

WinDbg

Python wrapper for DbgEng.

SWFRETools

example

Thomas Heller

http://sourceforge.net/projects/ctypes/ (In Python 2.5 it is already included)

ctypes is a Python module allowing to create and manipulate C data types in Python. These can then be passed to C-functions loaded from dynamic link libraries.

PyMem, WinAppDBG

official documentation
presentation "Using Cython to optimize Python and interface with C"
"API Hooking in Python"

Claudio “nex” Guarnieri

http://www.cuckoosandbox.org/

Cuckoo Sandbox is automated malware analysis system. It has API to customize both the processing and the reporting stages. Report contains information about network and filesystem activity, trace of assembler instructions can be obtained.

???

Documentation

Jurriaan Bremer (@skier_t)

https://github.com/jbremer/darm

Darm

A light-weight and efficient disassembler written in C for the ARMv7 instruction set.

Durmu

Description

Nektra

http://www.nektra.com/products/deviare-api-hook-windows/

Deviare

Deviare API is a professional API hook engine that was designed to create end user products. Intercepting applications is a complex task which can take place in many different scenarios.

Spy Studio

Windows API Hooking in Python with Deviare

distorm, Gil Dabah (arkon@ragestorm.net)

http://code.google.com/p/distorm/

A Fast Python Library for Reading PE+ Files.

???

???

distorm, Gil Dabah (arkon@ragestorm.net)

http://code.google.com/p/distorm/

diStorm3 binary stream disassembler library project.

???

API Hooking in Python

Philippe BIONDI (phil(at)secdev.org)

http://hg.secdev.org/elfesteem/

ELF/PE editing library.

Smiasm

???

Pierre-Marie de Rodat

https://bitbucket.org/pmderodat/frasm

The need of an assembler for a special architecture is not so unusual. When reverse-engineering some random machine or software, one often need to write an assembler: this enables one to produce bytecodes in order to test a virtual machine, or the behavior of some architecture.
FrASM aims to simplify and speed up the conception of simple assemblers: one need only to provide a description of the instruction set and their operands, maybe to write some hooks and to give opcode and binary format output code; FrASM takes care of lexing, parsing, sections sorting, symbols resolution and final binary output.

???

???

Manuel Fernandez

Francisco Oca

https://code.google.com/p/hookme/

HookMe

HookME is a software designed for intercepting communications by hooking the desired process and hooking the API calls for sending and receiving network data. HookMe have a plugins system in Python.

???

???

Gergely Erdelyi (http://gergelyerdelyi.com/)

Elias Bachaalany (@0xeb)

http://code.google.com/p/idapython/

IDA Pro (from 5.1)

IDAPython is an IDA Pro plugin that integrates the Python programming language, allowing scripts to run in IDA Pro. These programs have access to IDA Plugin API, IDC and all modules available for Python. The power of IDA Pro and Python provides a platform for easy prototyping of reverse engineering and other research tools.

IDA Toolbag
mynav
Dr. Gadget
rtti-helper-scripts
msdn-plugin-ida
ida2sql-plugin-ida
IDA file Patcher
Idagrapher
py-com-tools
Optimice

official documentation
IDAPython: User Scripting for a Complex Application
TOOLSMITHING AN IDA BRIDGE: A TOOL BUILDING CASE STUDY
blog entries about IDAPython
"Reverse Engineer's Cookbook" presentation
"Introduction to IDAPython" from OpenRCE

Immunity, Inc.

http://www.immunityinc.com/products-immdbg.shtml

ImmunityDebugger

Immunity Debugger's Python API includes many useful utilities and functions. Your scripts can be as integrated into the debugger as the native code. This means your code can create custom tables, graphs, and interfaces of all sorts that remain within the Immunity Debugger user experience.

pvefindaddr
mona

official documentation
presentation
cheatsheet by Corelan
forum

Immunity Inc., atlas (atlas@r4780y.com)

Matthew Carpenter (mcarpenter@intelguardians.com)

http://www.immunitysec.com/resources-freesoftware.shtml

Libdisassembly is simply a python library for disassembling x86 opcodes. It has been made for Immunity's PDB Project (a vulnerability development focused debugger), and is partially based on mammon libdisasm opcode list. There is still a lot of work to do with the Metadata, but the library tries to return as much information it can get off of an opcode.

???

???

University of Illinois/NCSA

http://lldb.llvm.org/

LLDB

lldb also has a built-in Python interpreter, which is accessible by the "script" command. All the functionality of the debugger is available as classes in the Python interpreter, so the more complex commands that in gdb you would introduce with the "define" command can be done by writing Python functions using the lldb-Python library, then loading the scripts into your running session and accessing them with the "script" command.

Example

API
"LLDB Modular Debugging Infrastructure" presentation
LLDB — Python Reference

???

http://www.llvmpy.org/

LLVM

llvmpy is a Python wrapper around the llvm C++ library which allows simple access to compiler tools. It can be used for a lot of things, but here are some ideas:
- dynamically create LLVM IR for linking with LLVM IR produced by CLANG or dragonegg
- build machine code dynamically using LLVM execution engine
- use together with PLY or other tokenizer and parser to write a complete compiler in Python

Bitey

???

Ronald Oussoren

http://pypi.python.org/pypi/macholib/

macholib can be used to analyze and edit Mach-O headers, the executable format used by Mac OS X.

???

Package Documentation

Serpilliere (serpilliere@droids-corp.org)

http://code.google.com/p/miasm/

http://code.google.com/p/smiasm/

Miasm is a a free and open source reverse engineering framework. Miasm aims at analyzing/modifying/generating binary programs. Miasm embed its own disassembler, intermediate language and instruction semantic. To emulate code, it uses libtcc to jit C code generate from intermediate representation. It can emulate shellcodes, parts of binaries. Python callback can be executed to emulate library functions.

smiasm

Miasm (incomprehensible documentation)

Georges BOSSERT (@Lapeluche) Frédéric GUIHERY (@_Sygus)

http://www.netzob.org

Netzob is an open source tool for reverse engineering, traffic generation and fuzzing of communication protocols. It allows to infer the message format and the state machine of a protocol through passive and active processes. The model can afterward be used to simulate realistic and controllable trafic.

???

API
Wiki

Scott Knight (knightsc@gmail.com)

http://code.google.com/p/ollypython/

OllyDbg

OllyPython is an OllyDbg plugin that integrates the Python programming language, allowing scripts to run in OllyDbg.

???

sample of use in entry blog

Brendan Dolan-Gavitt

http://code.google.com/p/pdbparse/

PDBparse is a GPL-licensed library for parsing Microsoft PDB files. Support for these is already available within Windows through the Debug Interface Access API, however, this interface is not usable on other operating systems.

???

???

???

http://code.google.com/p/w32-peel/

PEEL, with its ever-redundant project name, is a python-based library for manipulating and wrangling PE files.

???

???

Ero Carrera (@erocarrera)

http://code.google.com/p/pefile/

pefile is a multi-platform Python module to read and work with Portable Executable (aka PE) files. Most of the information in the PE Header is accessible, as well as all the sections, section's information and data. pefile requires some basic understanding of the layout of a PE file. Armed with it it's possible to explore nearly every single feature of the file.

IDA PEiD
peframe
PyPEELF

usage examples
usage examples
"Win32 Static Analysis in Python" presentation
"4 x 5: Reverse Engineering Automation with Python" presentation

Pedram Amini (@pedramamini)

http://code.google.com/p/paimei/ (part of PaiMei)

IDAPython, pGRAPH

Built on top of pGRAPH, PIDA aims to provide an abstract and persistent interface over binaries (DLLs and EXEs) with separate classes for representing functions, basic blocks and instructions. The end result is the creation of a portable file that when loaded allows you to arbitrarily navigate throughout the entire original binary.

PaiMei (http://code.google.com/p/paimei/)

< a href="http://pedram.redhive.com/PyDbg/docs/">official overview

Romain Gaucher (@rgaucher), Haris Andrianakis (@tl0gic)

https://github.com/neuroo/pinpy

PIN

PinPy essentially allows you to to run Python scripts inside whatever programs, just educate it using the XML config file, what you want to hook. You'll need to get some information so that pin can properly install the hooks such as signature, etc. This is done by embedding a Python runtime in a pin tool.

???

???

Roberto Paleari (@rpaleari)

Lorenzo Martignoni (@martignlo)

Lorenzo Cavallaro (http://www.few.vu.nl/~sullivan/)

http://code.google.com/p/processtap/

PinTool, (Valgrind, QEMU, DinamoRIO)

ProcessTap is a dynamic tracing framework for analyzing closed sourceapplications. ProcessTap is inspired by DTrace and SystemTap, but it is specific for analyzing closed-source user-space applications. ProcessTap leverages dynamic binary instrumentation to intercept the events of interest (e.g., function calls, system call, memory accesses, and conditional control transfers). Although the current implementation relies on PinTool, alternative back-ends for instrumentation (e.g., Valgrind, Qemu, or DynamoRIO) can be used. The language used in ProcessTap for writing scripts to instrument applications is Python.

???

examples

Grant Olson (kgo@grant-olson.net)

http://www.grant-olson.net/python/pyasm

Pyasm is a full-featured dynamic assembler written entirely in Python. By dynamic, I mean that it can be used to generate and execute machine code in python at runtime without requiring the generation of object files and linkage. It essentially allow 'inline' assembly in python modules on x86 platforms. Pyasm can also generate object files (for windows) like a traditional standalone assembler, although you're probably better off using one of the many freely available assemblers if this is you primary goal.

???

example
PyASM User's Guide

Felix Leder (felix.leder@googlemail.com)

Daniel Plohmann (daniel.plohmann@googlemail.com)

http://code.google.com/p/pyboxed/

PyBox (short for "Python Sandbox") is a flexible and light-weight process and system analysis framework. A user-level framework for rootkit-like monitoring of processes.

???

"PyBox — A Python approach to sandboxing"
wiki
"Do you know what’s happening in your ?" presentation

Adrián Manrique (@n0km, adrian@coresecurity.com)

Andrés López Luksenberg (aluksenberg@coresecurity.com)

http://corelabs.coresecurity.com/index.php?module=Wiki&action=view&type=...

QEMU

PyCodin is an open source Python library that allows instrumentation of low-level code for different architectures. It came out from the necessity of developing a testing environment for low-level code that exploits vulnerabilities (a.k.a. shellcode). The library provides a virtual CPU front-end, allowing the manipulation of a virtualized memory space and creating different
scenarios, giving the developer new tools to control the execution. PyCodin also allows runtime inspection and modification of the execution context of the instrumented program. The first version of the tool uses Qemu as the virtualization back-end.

???

"Pycodin: Instrumentando código sin dolor" presentation (spanish)

Ero Carrera (@erocarrera)

http://dkbza.org/pydasm.html

libdasm

pydasm is a python wrapper for libdasm. It attempts to capture all the functionality of libdasm and bring its versatility to Python.

PaiMei
PyPEELF

precompiled Windows binaries
"Win32 Static Analysis in Python" presentation
"4 x 5: Reverse Engineering Automation with Python" presentation

Rocky Bernstein

http://bashdb.sourceforge.net/pydb/

gdb

pydb is an expanded version of the Python debugger loosely based on the gdb command set and the stock Python debugger. It also has all of the features found in an earlier version of pydb.py that was distributed with the debugger GUI ddd.

???

official documentation

Pedram Amini (@pedramamini)

http://code.google.com/p/paimei/ (part of PaiMei)

PyDbg exposes most of the expected debugger functionality and then some. Hardware / software / memory breakpoints, process / module / thread enumeration and instrumentation, system DLL tracking, memory reading/writing and intelligent dereferencing, stack and SEH unwinding, exception and event handling, endian manipulation routines, memory snapshot
and restore functionality, disassembly (libdasm) engine. The abstracted interface allows for painless development of custom debugger scripts.

PaiMei
In Memory Fuzzing
Blocks
Pydbg64
egurra

official documentation
Hacking Leopard: Tools and Techniques for Attacking
Install PaiMei on Snow Leopard
How to use PyDbg as a powerful multitasking debugger
PaiMei on python25 (video)
Paimei From Svn, Idapython 0.8.0/Ida4.9Free, And Python 2.7.1 (video)

Botten, Michael Eddington (http://phed.org/)

Peter Silberman (@petersilberman)

http://sourceforge.net/projects/pydbgeng/

WinDdg

PyDbgEng is a Python Wrapper For Microsoft Debug Engine. Its features include: user mode debugging, kernel mode debugging, soft and hw breakpoints, symbol server and etc.

PyDbgExt
KStalker

usage examples
series of records in blog

Rocky Bernstein

http://code.google.com/p/pydbgr/

gdb

A rewrite of pydb from the ground up.

???

Installing and Using pydbgr

emilmont, Stefan Hladnik, Paul Harrington, Sebastien Colleur, Alan Au

http://code.google.com/p/pydevtools/

PyDevTools is a suite of python modules for the rapid prototyping of software development tools.

???

google group

Ero Carrera (@erocarrera)

http://code.google.com/p/pydot/

up to Graphviz 2.26.3

Python interface to Graphviz's Dot language. pydot allows to easily create both directed and non directed graphs from Python.

Generating Graph Visualizations with pydot and Graphviz (blog post)
graphviz documentation
homepage of pydot

???

Francois Lalande

Francois-Xavier Oxeda

Edouard Fajnzilberg

Kevin Szkudlapski

https://github.com/wisk/medusa

Medusa (http://eip.epitech.eu/2012/medusa/)

Medusa is an interractive disassembler available on multiple operating systems (MS Windows, GNU/Linux, *BSD, etc). It is a free software. Medusa permit to convert machine code into human readable entities, to apply heuristics in order to improve code clearness and to handle these heuristics to apply its own code analysis. Its modular design permit to handle
different executable file formats (PE, ELF, RAW, etc) and different architectures (Intel, ARM, etc) by the means of plugins. Differents views are usable in the graphical user interface. The views permit to see the character strings in the executable file, the list of imported and exported functions, etc. One example of a view, the control flow graph, allows for better viewing of the different parts of the execution flow and therefore to undertand more quickly the internal mechanism of the executable file.

???

???

Roberto Paleari (@rpaleari)

Lorenzo Martignoni (@martignlo)

http://roberto.greyhats.it/projects.html

PyEA (Python Executable Analyser) is a hybrid static/dynamic code analyser written in Python. The analyser was originally developed to statically analyse IA-32 malicious programs, but has soon evolved into a generic analyser for compiled programs. PyEA currently supports PE and ELF executables, disassembles executables using a recursive disassembler, and translates each machine instruction into an intermediate form, that makes side effects explicit.

???

???

Ben Leslie

http://ertos.nicta.com.au/software/kenge/pyelf/devel/

PyELF library allows the parsing and manipulation of ELF objects in a platform and toolchain independant manner. It is primarily designed for the Kenge build system, but would form a great basis for a general purpose Python ELF library.

PyPEELF

???

Eli Bendersky (eliben@gmail.com)

https://bitbucket.org/eliben/pyelftools

pyelftools is a pure-Python library for parsing and analyzing ELF files and DWARF debugging information. It provides both low-level and high-level APIs for querying ELF and DWARF, and is mostly feature-complete.

???

user guide

Cody Pierce (@codypierce)

http://code.google.com/p/pyemu/

PyEmu tries to provide a fully scriptable IA-32 emulator in python. The aim is for security researchers and malware analysis. By having a flexible community driven emulator in a high level language one can roll their own purpose driven scripts to solve common problems.

???

whitepaper from BH USA 07
video from BH USA 07
entry in blog about usage PyEMU

Joxean Piti

http://code.google.com/p/pyew/

Pyew is a (command line) python tool like radare and *iew oriented, mainly, to analyze malware. It does have support for hexadecimal viewing, disassembly (Intel 16, 32 and 64 bits), PE and ELF file formats (it does code analysis the right way), following direct call/jmp instructions, OLE2 format, PDF format (limited) and more. It also supports plugins to add more features to the tool.

???

entries in blog about usage pyew

Michael Eddington (mike@phed.org)

Frank Laub (frank.laub@gmail.com)

http://code.google.com/p/pygdb/

gdb

This is a simple python wrapper around GDB. pygdb is a pygtk interface to gdb. It offers two terminal windows, one for gdb, one for the process to be debugged. On the top it has standard buttons like run, continue, step in, step over, step out and quit. On a second window you can add watches and breakpoints. Furthermore, you can inspect the backtrace and launch gvim on the current executed line by pressing a button. pygdb stays synchronized with gvim (by using gvim --servername calls).

???

???

Elias Bachaalany (@0xeb)

http://code.google.com/p/pyhiew/

HIEW

PyHiew is a Hiew External Module that allows users to write Python scripts that interface with Hiew.

???

entries in blog about usage pyHIEW

Team (http://pykd.codeplex.com/team/view)

http://pykd.codeplex.com/

WinDBG

Python extension for WinDbg. pykd not repeat functional from Debug Engine, and implements the API, convenient for daily work in WinDbg.

???

official documentation
blog about pykd (RU)

Angelo Dell'Aera (buffer@antifork.org, @angelodellaera)

https://github.com/buffer/pylibemu

Libemu

Pylibemu is a wrapper for the Libemu library.

???

Shellcode Detection Using Python

Georg Wicherski (@ochsff): http://code.mwcollect.org/projects/pylibscizzle

http://code.mwcollect.org/projects/pylibscizzle

libscizzle

Identification of possible getpc sequences, bruteforce possible starting location around sequence, use efficient sandbox. Disassemble guest code, execute one basic blocks, emulate all other instructions, exception.

???

Efficient Bytecode Analysis: Linespeed Shellcode Detection
Shellcode Detection Using Python

Fabien Reboia (srounet@gmail.com)

https://github.com/srounet/Pymem

Pymem is a memory wrapper built on top of python ctypes and windll imports to facilitate process memory access in Read or Write. It has functionalities such as Opening a process in debug mode, hijacking threads, listing process modules and much more.

???

code example

Matthieu Kaczmarek (tecamac@gmail.com)

Daniel Reynaud (reynaud.daniel@gmail.com)

http://code.google.com/p/pymsasid/

Pym's is a pure python disassembly library. It is merely a port of udis86 to python.

???

online disassemble
project with setup

Rich Smith (mynameismeerkat@gmail.com)

http://code.google.com/p/pyretic/

pyREtic and the REpdb debugger allow easier access to obtaining source from closed source Python applications. In a nutshell it allows you to take a object in memory back to source code, without needing access to the bytecode directly on disk. This can be useful if the applictions pyc's on disk are obfuscated in one of many ways.

???

whitepaper
slides from BlackHat/Defcon 2010

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.

???

???

Ryan Brady

https://github.com/rbrady/python-adb

python-adb is an MIT-licensed, open source python library to integrate some features from the Android Debug Bridge.

???

???

Loïc Jaquemet (loic.jaquemet@gmail.com)

http://pypi.python.org/pypi/haystack

https://github.com/trolldbois/python-haystack/

ctypes, python-ptrace, WinAppDbg

The basic functionality is to search in a process' memory maps for a specific C Structures.

sslsnoop
ctypes-kernel

???

Victor Stinner (@victor_stinner)

http://pypi.python.org/pypi/python-ptrace

python-ptrace is a debugger using ptrace (Linux, BSD and Darwin system call to trace processes) written in Python.

Fuzil

wiki

???

http://sourceware.org/gdb/wiki/PythonGdb (In gdb 7 it is already included)

Gdb

Integrate Python scripting into Gdb.

gdbxx
gdb-heap
runFuzzer
tmalloc_gdb
GDB-Python-Utils
PEDA

official tutorial
API
entry in blog
presentation from PyCON US 2011
In-memory-fuzzing in Linux (with GDB and Python)
Debugging C/C++ and CPython using GDB 7?s new Python extension support
overview of the Python API accessible from GDB
http://blog.lse.epita.fr/articles/10-pythongdb-tutorial-for-reverse-engineering---part-.html

Rocky Bernstein (rocky@gnu.org)

http://code.google.com/p/pytracer/

A more flexible interface to sys.settrace allowing, for example, chained trace hooks. We allow several trace hooks to get registered and unregistered and allow tracing to be turned on and off temporarily without losing the trace hooks. You can also indicate filters on events for which trace hooks should fire and mark methods that should automatically be ignored.

???

???

Bryan Payne

https://code.google.com/p/vmitools

LibVMI

LibVMI is an introspection library focused on reading and writing memory from virtual machines (VMs). For convienence, LibVMI also provides functions for accessing CPU registers, pausing and unpausing a VM, printing binary data, and more. LibVMI is designed to work across multiple virtualization platforms. LibVMI currently supports VMs running in either Xen or KVM. LibVMI also supports reading physical memory snapshots when saved as a file.

???

???

pancake (http://nopcode.org)

nibble.ds

earada (@earada)

http://radare.org/doc/html/Section10.6.html#python

radare2

The second scripting language implemented in radare was 'python'. The python interface for C is not as nice as the LUA one, and it is obviously not as optimal as LUA, but it gives a very handy syntax and provides a full-featured list of libraries and modules to extend your script.

???

radare official site

Stephane Duverger

https://github.com/sduverger/ramooflax

Ramooflax is a pre-boot virtualization tool. Ramooflax aims at analyzing/debugging/controlling modern operating systems and complex software pieces as well as real life BIOS running on a physical machine. Ramooflax provides a small hypervisor and a remote client allowing high-level access to the features implemented into the hypervisor.

???

???

Core Security Technologies

http://oss.coresecurity.com/projects/uhooker.htm

OllyDBG 1.10

The Universal Hooker is a tool to intercept execution of programs. It enables the user to intercept calls to API calls inside DLLs, and also arbitrary addresses within the executable file in memory.

???

official documentation
usage

invisigoth kenshoto (@invisig0th)

https://www.kenshoto.com/wiki/index.php/Main_Page

Vivisect is programatic binary analysis framework.
Features:
* Simple/fast python API for trying out crazy analysis ideas
* Complete emulation pass with annotation
* Import emulation to allow emu state tracking
* Analysis of Elf/PE/binaryblob formats (Mach-O to come soon)
* Support for easy to implement and batch run analysis module interface
* Support for more than one binary file loaded in one workspace
* Colaborative real-time client/server mode
* Reasonably decent GUI (mostly for viewing) results
* Support for running on windows/linux/mac
* Windows symbol server support (when run on win32)
* Bulk analysis mode which goes nice and fast (w/o GUI)

???

Visipedia
Examples

invisigoth kenshoto (@invisig0th)

http://code.google.com/p/vtrace-mirror/

vtrace is a cross-platform debugging api written in python. Each supported platform has it's own support module.

vdebug

entry in blog
vtrace script examples
MindshaRE: Another Approach To Tracking ReadFile

Mario Vilas (@Mario_Vilas)

http://winappdbg.sourceforge.net/

The WinAppDbg python module allows developers to quickly code instrumentation scripts in Python under a Windows environment.

Tools
PyPEELF

programming guide

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.

???

guide