Tools Using STP

STP has been used in over 100 research projects. We know this based on Google scholar citations and STP user emails. Around 25 projects are listed below.

Bug Finding and Symbolic Execution Tools

    • EXE is a bug finding tool that reads your C program and tries to automatically crash it. EXE has been used to find bugs in TCP/IP Filters, Berkeley Packet Filter,  Linux Disks, PCRE library. This work is being done by Cristian Cadar, Vijay Ganesh, Peter Pawlowski, Prof. Dawson Engler and Prof. David Dill at Stanford University
    • Klee is a bug finding tool from Professor Dawson Engler's group at Stanford University
    • MINESWEEPER  is a tool that automatically analyzes certain malicious behavior in unix utilities and malware. This work is being done by Jim Newsome, David Brumley, Prof. Dawn Song and others at Carnegie Mellon University (CMU)
    • CATCHCONV is a bug finding tool that tries to find bugs due to type mismatch in C programs. This work is being done by David Molnar and Prof. David Wagner at University of California, Berkeley

    • Backward path-sensitive analysis of C programs to find bugs by Tim Leek from MIT Lincoln Labs

    • Bug finding in Verilog code by a major microprocessor company

BlueSpec Hardware/Software Co-synthesis Tool using  STP

    • The BlueSpec Hardware/Software Compiler company is using STP at its primary backend SMT solver (source of information: Dr. Nirav Dave of SRI International and MIT)

Formal Verification Tools

    • In conjunction with ACL2 to formally verify implementation of encryption algorithms in Java by Eric W. Smith and Prof. David Dill at Stanford University
    • Formal verification of Parallel Transaction Architecture by Jacob Chang and Prof. David Dill at Stanford University

Tools For Finding Security Exploits

    • REPLAYER is a tool that replays an application dialog between two hosts in order to analyze security exploits by Jim Newsome, David Brumley, Prof. Dawn Song and others at Carnegie Mellon University (CMU)
    • "smart fuzzing" prototype for the automatic detection of security vulnerabilities in executable code

    • Hampi : A solver for string constraints (This is being used to automatically construct SQL injection and XSS exploits) by Adam Kiezun, Vijay Ganesh and Michael Ernst at MIT

    • STP is being used at Akamai to find security errors in infra-critical software

Other ongoing projects using STP

    • Program Analysis by DiptiKalyan Saha (
    • Program Analysis by Professor Rupak Majumdar's group at UCLA
    • Kiasan symbolic execution tool by Professor Deng's group at Penn State University
    • Professor David Brumley's group at Carnegie Mellon University
    • Sebastian Gfeller at EPFL, Switzerland
    • Trevor Alexander Hansen at University of Melbourne, Australia
    • WangTie Lei at Peking University, Beijing, China
    • Government information assurance labs
    • Tommi Juntilla at Helsinki University of Technology, Finland
    • Lorenzo Martignoni at University of Wisconsin, Madison, USA
    • Hardware Model Checking by Mike Katelman and Nirav Dave at MIT
    • Gabriel Campana at

Simplifying Development of Distributed Systems using STP

    • Prophet (Development and deployment of Distributed Systems) by Dejan Kostic at EPFL, Switzerland

Automatic Configuration Tool using STP

    • Tvl2STP from University of Namur in Belgium (Raphael Michel, Arnaud Hubaux, Patrick Heymans, and Vijay Ganesh)