STP Main Page

STP Papers

Tools Using STP

STP Documentation

Projects Using STP

• 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


• JPF-SE is a symbolic execution extension to the Java PathFinder model checker by Saswat Anand, Corina Pasareanu and Willem Visser from NASA Ames Research Center
  

• 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 equations over regular expressions (This is being used to automatically construct SQL injection and XSS exploits) by Adam Kiezun, Vijay Ganesh and Michael Ernst at MIT

• Other ongoing projects using STP

• Program Analysis by DiptiKalyan Saha (diptikalyan@gmail.com)

• 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

• Mike Katelman and Nirav Dave at MIT

• Gabriel Campana at security-labs.org

• Proposed Projects

• Using STP for Program Sketching by Professor Armando Solar-Lezama at MIT