<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
<style>BODY, P, DIV, H1, H2, H3, H4, H5, H6, ADDRESS, OL, UL, LI, TITLE, TD, OPTION, SELECT
{
font-family: Verdana
}
BODY, P, DIV, ADDRESS, OL, UL, LI, TITLE, TD, OPTION, SELECT
{
font-size: 10.0pt;
margin-top:0pt;
margin-bottom:0pt;
}
BODY, P
{
margin-left:0pt;
margin-right:0pt;
}
BODY
{
background: white;
margin: 6px;
padding: 0px;
}
h6 { font-size: 10pt }
h5 { font-size: 11pt }
h4 { font-size: 12pt }
h3 { font-size: 13pt }
h2 { font-size: 14pt }
h1 { font-size: 16pt }
blockquote { padding: 10px; border: 1px #DDDDDD dashed }
a img { border: 0; }
table.zeroBorder {
border-width: 1px 1px 1px 1px;
border-style: dotted dotted dotted dotted;
border-color: gray gray gray gray;
}
table.zeroBorder th {
border-width: 1px 1px 1px 1px;
border-style: dotted dotted dotted dotted;
border-color: gray gray gray gray;
}
table.zeroBorder td {
border-width: 1px 1px 1px 1px;
border-style: dotted dotted dotted dotted;
border-color: gray gray gray gray;
}
.hiddenStyle {
visibility: hidden;
position: absolute;
z-Index: 1;
paddingRight: 0;
background: white
}
.misspell { background-image: url('/images/misspell.gif'); background-repeat: repeat-x; background-position: bottom }
@media screen {
.pb { border-top: 1px dashed #C0C0C0; border-bottom: 1px dashed #C0C0C0 }
.writely-comment { font-size: 9pt; line-height: 1.4em; padding: 1px; border: 1px dashed #C0C0C0 }
}
@media print {
.pb { border-top: 0px; border-bottom: 0px }
.writely-comment { display: none }
}
@media screen,print {
.pb { height: 1px }
}
</style>
<title>Tools Using STP</title>
</head>
<body revision="ddvbwkf4_12dp5n4m:8">
<h2 style="text-align: center; color: rgb(153, 0, 0);"><big><big> <font
size="5"><big><big>STP</big></big></font>
</big></big></h2>
<div style="text-align: center; color: rgb(153, 0, 0);">
<h2><font style="color: rgb(153, 0, 0);" size="5">A Decision Procedure
for
Bitvectors and Arrays</font></h2>
</div>
<table style="text-align: left;" border="0" cellpadding="10"
cellspacing="20">
<tbody>
<tr>
<td style="vertical-align: top; text-align: left;">
<h4><a href="stp.html">STP Main Page</a></h4>
<h4><a href="stp-papers.html">STP Papers</a></h4>
<h4><a href="stp-tools.html">Tools Using STP<br>
</a></h4>
<h4><a href="stp-docs.html">STP_Documentation</a></h4>
</td>
<td style="vertical-align: top;">
<h2><span style="color: rgb(153, 51, 153);">Projects that use STP</span></h2>
<ul>
<li><span style="font-weight: bold;">Bug Finding and Symbolic
Execution Tools</span></li>
</ul>
<span style="font-weight: bold;"><br>
</span>
<ul>
<ul>
<li><a href="exe.pdf">EXE</a> 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 <span style="font-weight: bold;">Stanford
University</span> <br>
</li>
</ul>
</ul>
<br>
<ul>
<ul>
<li><a href="http://www.ece.cmu.edu/%7Edawnsong/">MINESWEEPER</a>
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 <span style="font-weight: bold;">Carnegie
Mellon University (CMU)</span><br>
</li>
</ul>
</ul>
<br>
<ul>
<ul>
<li>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 <span style="font-weight: bold;">University
of
California, Berkeley</span></li>
</ul>
</ul>
<br>
<ul>
<ul>
<li>Backward path-sensitive analysis of C programs to find
bugs by
Tim Leek from <span style="font-weight: bold;">MIT Lincoln Labs</span></li>
</ul>
</ul>
<br>
<ul>
<ul>
<li>Bug finding in <span style="font-weight: bold;">Verilog</span>
code by a major <span style="font-weight: bold;">microprocessor company</span></li>
</ul>
</ul>
<br>
<ul>
<ul>
<li><a
href="http://ase.arc.nasa.gov/people/pcorina/papers/jpfseTACAS07.pdf">JPF-SE</a>
is a symbolic execution extension to the <a
href="http://javapathfinder.sourceforge.net/">Java PathFinder</a>
model checker by Saswat Anand, Corina Pasareanu and Willem Visser from <span
style="font-weight: bold;">NASA Ames Research Center</span><br>
</li>
</ul>
</ul>
<br>
<ul>
<li><span style="font-weight: bold;">Formal Verification Tools</span></li>
</ul>
<span style="font-weight: bold;"><br>
</span>
<ul>
<ul>
<li>In conjunction with <a
href="http://www.cs.utexas.edu/users/moore/acl2/">ACL2</a> to formally
verify implementation of encryption algorithms in Java by Eric W. Smith
and Prof. David Dill at <span style="font-weight: bold;">Stanford
University</span><br>
</li>
</ul>
</ul>
<br>
<ul>
<ul>
<li>Formal verification of Parallel Transaction Architecture
by
Jacob
Chang and Prof. David Dill at <span style="font-weight: bold;">Stanford
University</span><br>
</li>
</ul>
</ul>
<br>
<ul>
<li style="font-weight: bold;">Tools For Finding Security
Exploits</li>
</ul>
<br>
<ul style="font-weight: bold;">
<ul>
<li><a style="font-weight: normal;"
href="http://www.ece.cmu.edu/%7Ejnewsome/">REPLAYER</a><span
style="font-weight: normal;"> is a
tool that replays an application dialog between two hosts in order to
find security exploits by Jim Newsome, David Brumley, Prof. Dawn Song
and others at <span style="font-weight: bold;">Carnegie Mellon
University (CMU)</span></span></li>
</ul>
</ul>
<div style="margin-left: 40px;"> </div>
</td>
</tr>
</tbody>
</table>
<a href="#stp"></a><br>
</body>
</html>
distrib
>
Fedora
>
14
>
x86_64
>
media
>
os
>
by-pkgid
>
e4284596e3656e403aa4a54f4fcd0ae3
>
files
>
11
