+++ /dev/null
-<!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>STP Documentation</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>
- <br>
- </td>
- <td style="vertical-align: top;">
- <h2 style="color: rgb(102, 102, 0);">Input Language of STP</h2>
- <h3>Introduction</h3>
- <p>STP is an efficient decision procedure for the validity (or
-satisfiability) of formulas from a quantifier-free many-sorted theory
-of fixed-width bitvectors and (non-extensional) one-dimensional arrays.
-The functions in STP's input language include concatenation,
-extraction, left/right shift, sign-extension, unary minus, addition,
-multiplication, (signed) modulo/division, bitwise Boolean operations,
-if-then-else terms, and array reads and writes. The predicates in the
-language include equality and (signed) comparators between bitvector
-terms.<br>
- <br>
-The basic architecture of STP essentially follows the idea of
-word-level preprocessing followed by translation to SAT (We use
-MINISAT). In particular, we introduce several new heuristics for the
-preprocessing step, including abstraction-refinement in the context of
-arrays, a new bitvector linear arithmetic equation solver, and some
-interesting simplifications. These heuristics help us acheive several
-magnitudes of order performance over other tools, and also over
-straight-forward translation to SAT. STP has been heavily tested on
-thousands of examples sourced from various real-world applications such
-as program analysis and bug-finding tools like EXE, and equivalence
-checking tools and theorem-provers. <br>
- </p>
- <h3>The Input Langauge<br>
- </h3>
- <h4 style="margin-left: 40px;">Declarations<br>
- </h4>
- <div style="margin-left: 40px;">Bit-vector expressions (or terms)
-are
-constructed out of bit-vector
-constants, bit-vector variables and the functions listed below. In STP
-all variables have to declared before the point of use. An example
-declaration of a bit-vector variable of length, say 32, is as follows: </div>
- <div style="margin-left: 40px;" class="fragment">
- <pre class="fragment">x : BITVECTOR(32);<br></pre>
- </div>
- <p style="margin-left: 40px;">An example of an array declaration
-is as
-follows:</p>
- <pre style="margin-left: 40px;" class="fragment">x_arr : ARRAY BITVECTOR(32) OF BITVECTOR(5000);<br><br></pre>
- <h4 style="margin-left: 40px;">Functions
-and Terms<br>
- </h4>
- <p style="margin-left: 40px;">Bit-vector variables (or terms) of
-length
-0 are not allowed.
-Bit-vector
-constants can be represented in binary or hexadecimal format. The
-rightmost bit is called the least significant bit (LSB), and the
-leftmost bit is the most significant bit(MSB). The index of the LSB is
-0, and the index of the MSB is n-1 for an n-bit constant. This
-convention naturally extends to all bit-vector expressions. Following
-are some examples of bit-vector constants:</p>
- <div style="margin-left: 40px;" class="fragment">
- <pre class="fragment">0bin0000111101010000, and the corresponding hex representation is 0hex0f50.<br></pre>
- </div>
- <p style="margin-left: 40px;">The Bit-vector implementation in
-STP
-supports a very large number
-of functions and predicates. The functions are categorized into
-word-level functions, bitwise functions, and arithmetic functions. Let
-t1,t2,...,tm denote some arbitrary bitvector terms<span
- style="font-family: mon;"><span style="font-weight: bold;">. </span></span></p>
- <p style="margin-left: 40px;"><span style="font-family: mon;"><span
- style="font-weight: bold;"></span></span><span
- style="font-weight: bold;">The word level functions are:</span><br>
- </p>
- <div style="margin-left: 40px;" class="fragment">
- <table style="text-align: left; width: 680px; height: 316px;"
- border="1" cellpadding="2" cellspacing="2">
- <tbody>
- <tr>
- <td style="vertical-align: top;">Name<br>
- </td>
- <td style="vertical-align: top;">Symbol<br>
- </td>
- <td style="vertical-align: top;">Example<br>
- </td>
- </tr>
- <tr>
- <td style="vertical-align: top;">Concatenation<br>
- </td>
- <td style="vertical-align: top;">@<br>
- </td>
- <td style="vertical-align: top;">t1@t2@...@tm<br>
- </td>
- </tr>
- <tr>
- <td style="vertical-align: top;">Extraction<br>
- </td>
- <td style="vertical-align: top;">[i:j]<br>
- </td>
- <td style="vertical-align: top;">x[31:26]<br>
- </td>
- </tr>
- <tr>
- <td style="vertical-align: top;">left shift<br>
- </td>
- <td style="vertical-align: top;"><<<br>
- </td>
- <td style="vertical-align: top;">0bin0011 << 3 =
-0bin0011000<br>
- </td>
- </tr>
- <tr>
- <td style="vertical-align: top;">right shift<br>
- </td>
- <td style="vertical-align: top;">>><br>
- </td>
- <td style="vertical-align: top;">x[24:17] >> 5,
-another
-example: 0bin1000 >> 3 = 0bin0001</td>
- </tr>
- <tr>
- <td style="vertical-align: top;">sign extension<br>
- </td>
- <td style="vertical-align: top;">BVSX(bv,n)<br>
- </td>
- <td style="vertical-align: top;">BVSX(0bin100, 5) =
-0bin11100</td>
- </tr>
- <tr>
- <td style="vertical-align: top;">Array READ<br>
- </td>
- <td style="vertical-align: top;">[index]<br>
- </td>
- <td style="vertical-align: top;">x_arr[t1]<br>
- </td>
- </tr>
- <tr>
- <td style="vertical-align: top;">Array WRITE<br>
- </td>
- <td style="vertical-align: top;">WITH<br>
- </td>
- <td style="vertical-align: top;">x_arr WITH [index] := value<br>
- </td>
- </tr>
- </tbody>
- </table>
- </div>
- <ul style="margin-left: 40px;">
- <li>For extraction terms, say t[i:j], n > i >= j >= 0,
-where
-n is the length of t.</li>
- <li>For Left shift terms, t << k is equal to k 0's
-appended to
-t. The length of t << k is n+k.</li>
- <li>for
-Right shift terms, say t >> k, the term is equal to the bitvector
-obtained by k 0's followed by t[n-1:k]. The length of t >> k is n.</li>
- </ul>
- <div style="margin-left: 40px;"><span style="font-weight: bold;">The
-bitwise functions are:</span><br style="font-weight: bold;">
- </div>
- <br>
- <div style="margin-left: 40px;">
- <table style="text-align: left; width: 684px; height: 242px;"
- border="1" cellpadding="2" cellspacing="2">
- <tbody>
- <tr>
- <td style="vertical-align: top;">Name<br>
- </td>
- <td style="vertical-align: top;">Symbol<br>
- </td>
- <td style="vertical-align: top;">Example<br>
- </td>
- </tr>
- <tr>
- <td style="vertical-align: top;">Bitwise AND<br>
- </td>
- <td style="vertical-align: top;">&<br>
- </td>
- <td style="vertical-align: top;">t1 & t2 & ...
-& tm<br>
- </td>
- </tr>
- <tr>
- <td style="vertical-align: top;">Bitwise OR<br>
- </td>
- <td style="vertical-align: top;">|<br>
- </td>
- <td style="vertical-align: top;">t1 | t2 | t3 | ... | tm<br>
- </td>
- </tr>
- <tr>
- <td style="vertical-align: top;">Bitwise NOT<br>
- </td>
- <td style="vertical-align: top;">~<br>
- </td>
- <td style="vertical-align: top;">~t1<br>
- </td>
- </tr>
- <tr>
- <td style="vertical-align: top;">Bitwise XOR<br>
- </td>
- <td style="vertical-align: top;">BVXOR<br>
- </td>
- <td style="vertical-align: top;">BVXOR(t1,t2)<br>
- </td>
- </tr>
- <tr>
- <td style="vertical-align: top;">Bitwise NAND<br>
- </td>
- <td style="vertical-align: top;">BVNAND<br>
- </td>
- <td style="vertical-align: top;">BVNAND(t1,t2)<br>
- </td>
- </tr>
- <tr>
- <td style="vertical-align: top;">Bitwise NOR<br>
- </td>
- <td style="vertical-align: top;">BVNOR<br>
- </td>
- <td style="vertical-align: top;">BVNOR(t1,t2)<br>
- </td>
- </tr>
- <tr>
- <td style="vertical-align: top;">Bitwise XNOR<br>
- </td>
- <td style="vertical-align: top;">BVXNOR<br>
- </td>
- <td style="vertical-align: top;">BVXNOR(t1,t2)<br>
- </td>
- </tr>
- </tbody>
- </table>
- <br>
- <ul>
- <li>It is required that all the arguments of bitwise functions
-have
-the same length</li>
- </ul>
- <span style="font-weight: bold;">The arithmetic functions are:<br>
- </span>
- <table style="text-align: left; width: 692px; height: 314px;"
- border="1" cellpadding="2" cellspacing="2">
- <tbody>
- <tr>
- <td style="vertical-align: top;">Name<br>
- </td>
- <td style="vertical-align: top;">Symbol<br>
- </td>
- <td style="vertical-align: top;">Example<br>
- </td>
- </tr>
- <tr>
- <td style="vertical-align: top;">Bitvector Add<br>
- </td>
- <td style="vertical-align: top;">BVPLUS<br>
- </td>
- <td style="vertical-align: top;">BVPLUS(n,t1,t2,...,tm)<br>
- </td>
- </tr>
- <tr>
- <td style="vertical-align: top;">Bitvector Mult<br>
- </td>
- <td style="vertical-align: top;">BVMULT<br>
- </td>
- <td style="vertical-align: top;">BVMULT(n,t1,t2)<br>
- </td>
- </tr>
- <tr>
- <td style="vertical-align: top;">Bitvector subtract<br>
- </td>
- <td style="vertical-align: top;">BVSUB<br>
- </td>
- <td style="vertical-align: top;">BVSUB(n,t1,t2)<br>
- </td>
- </tr>
- <tr>
- <td style="vertical-align: top;">Bitvector Unary Minus<br>
- </td>
- <td style="vertical-align: top;">BVUMINUS<br>
- </td>
- <td style="vertical-align: top;">BVUMINUS(t1)<br>
- </td>
- </tr>
- <tr>
- <td style="vertical-align: top;">Bitvector Div<br>
- </td>
- <td style="vertical-align: top;">BVDIV<br>
- </td>
- <td style="vertical-align: top;">BVDIV(n,t1,t2), where t1
-is the
-dividend and t2 is the divisor<br>
- </td>
- </tr>
- <tr>
- <td style="vertical-align: top;">Signed Bitvector Div<br>
- </td>
- <td style="vertical-align: top;">SBVDIV<br>
- </td>
- <td style="vertical-align: top;">SBVDIV(n,t1,t2), where t1
-is the
-dividend and t2 is the divisor</td>
- </tr>
- <tr>
- <td style="vertical-align: top;">Bitvector Modulo<br>
- </td>
- <td style="vertical-align: top;">BVMOD<br>
- </td>
- <td style="vertical-align: top;">BVMOD(n,t1,t2), where t1
-is the
-dividend and t2 is the divisor</td>
- </tr>
- <tr>
- <td style="vertical-align: top;">Signed Bitvector Modulo<br>
- </td>
- <td style="vertical-align: top;">SBVREM<br>
- </td>
- <td style="vertical-align: top;">SBVREM(n,t1,t2), where t1
-is the
-dividend and t2 is the divisor</td>
- </tr>
- </tbody>
- </table>
- <span style="font-weight: bold;"></span></div>
- <ul style="margin-left: 40px;">
- <li>the number of output bits has to specified (except unary
-minus).</li>
- <li>Inputs t1,t2 ...,tm must be of the same length<br>
- </li>
- <li>BVUMINUS(t) is a short-hand for BVPLUS(n,~t,0bin1), where n
-is
-the length of t.</li>
- <li>Bitvector subtraction (BVSUB(n,t1,t2)) is a short-hand for
-BVPLUS(n,t1,BVUMINUS(t2))</li>
- </ul>
- <p style="margin-left: 40px;">STP also supports conditional terms
-(IF cond THEN t1 ELSE t2
-ENDIF), where cond is boolean term, t1 and t2 can be bitvector terms.
-This allows us to simulate multiplexors. An example is:</p>
- <div class="fragment">
- <pre style="margin-left: 40px;" class="fragment">x,y : BITVECTOR(1);<br>QUERY(x = IF 0bin0=x THEN y ELSE BVUMINUS(y));<br></pre>
- </div>
- <h4 style="margin-left: 40px;">Predicates<br>
- </h4>
- <div class="fragment">
- <div style="margin-left: 40px;">Following are the predicates
-supported
-by STP:<br>
- </div>
- <div style="margin-left: 40px;"><br>
- </div>
- <table
- style="text-align: left; width: 676px; height: 390px; margin-left: 40px;"
- border="1" cellpadding="2" cellspacing="2">
- <tbody>
- <tr>
- <td style="vertical-align: top;">Name<br>
- </td>
- <td style="vertical-align: top;">Symbol<br>
- </td>
- <td style="vertical-align: top;">Example<br>
- </td>
- </tr>
- <tr>
- <td style="vertical-align: top;">Equality<br>
- </td>
- <td style="vertical-align: top;">=<br>
- </td>
- <td style="vertical-align: top;">t1=t2<br>
- </td>
- </tr>
- <tr>
- <td style="vertical-align: top;">Less Than<br>
- </td>
- <td style="vertical-align: top;">BVLT<br>
- </td>
- <td style="vertical-align: top;">BVLT(t1,t2)<br>
- </td>
- </tr>
- <tr>
- <td style="vertical-align: top;">Greater Than<br>
- </td>
- <td style="vertical-align: top;">BVGT<br>
- </td>
- <td style="vertical-align: top;">BVGT(t1,t2)<br>
- </td>
- </tr>
- <tr>
- <td style="vertical-align: top;">Less Than Or Equal To<br>
- </td>
- <td style="vertical-align: top;">BVLE<br>
- </td>
- <td style="vertical-align: top;">BVLE(t1,t2)<br>
- </td>
- </tr>
- <tr>
- <td style="vertical-align: top;">Greater Than Or Equal To<br>
- </td>
- <td style="vertical-align: top;">BVGE<br>
- </td>
- <td style="vertical-align: top;">BVGE(t1,t2)<br>
- </td>
- </tr>
- <tr>
- <td style="vertical-align: top;"><br>
- </td>
- <td style="vertical-align: top;"><br>
- </td>
- <td style="vertical-align: top;"><br>
- </td>
- </tr>
- <tr>
- <td style="vertical-align: top;">Signed Less Than<br>
- </td>
- <td style="vertical-align: top;">SBVLT<br>
- </td>
- <td style="vertical-align: top;">SBVLT(t1,t2)<br>
- </td>
- </tr>
- <tr>
- <td style="vertical-align: top;">Signed Greater Than<br>
- </td>
- <td style="vertical-align: top;">SBVGT<br>
- </td>
- <td style="vertical-align: top;">SBVGT(t1,t2)<br>
- </td>
- </tr>
- <tr>
- <td style="vertical-align: top;">Signed Less Than Or Equal
-To<br>
- </td>
- <td style="vertical-align: top;">SBVLE<br>
- </td>
- <td style="vertical-align: top;">SBVLE(t1,t2)<br>
- </td>
- </tr>
- <tr>
- <td style="vertical-align: top;">Signed Greater Than Or
-Equal To<br>
- </td>
- <td style="vertical-align: top;">SBVGE<br>
- </td>
- <td style="vertical-align: top;">SBVGE(t1,t2)<br>
- </td>
- </tr>
- </tbody>
- </table>
- <div style="margin-left: 40px;">
- <ul>
- <li>STP requires that in atomic formulas such
-as x=y, x and y are expressions of the same length. STP accepts Boolean
-combination of atomic formulas.</li>
- </ul>
- </div>
- <h3>Some
-Examples</h3>
- </div>
- <p style="margin-left: 40px;"><span style="font-weight: bold;">Example
-1</span>
-illustrates the use of arithmetic, word-level and bitwise
-NOT operations:</p>
- <div style="margin-left: 40px;" class="fragment">
- <pre class="fragment">x : BITVECTOR(5);<br>y : BITVECTOR(4);<br>yy : BITVECTOR(3);<br>QUERY(<br> BVPLUS(9, x@0bin0000, (0bin000@(~y)@0bin11))[8:4] = BVPLUS(5, x, ~(y[3:2])) <br>);<br></pre>
- </div>
- <p style="margin-left: 40px;"><span style="font-weight: bold;">Example
-2 </span>illustrates the use of arithmetic, word-level and
-multiplexor terms:</p>
- <div style="margin-left: 40px;" class="fragment">
- <pre class="fragment">bv : BITVECTOR(10);<br>a : BOOLEAN;<br>QUERY(<br>0bin01100000[5:3]=(0bin1111001@bv[0:0])[4:2] <br>AND <br>0bin1@(IF a THEN 0bin0 ELSE 0bin1 ENDIF)=(IF a THEN 0bin110 ELSE 0bin011 ENDIF)[1:0]<br>);<br></pre>
- </div>
- <p style="margin-left: 40px;"><span style="font-weight: bold;">Example
-3</span>
-illustrates the use of bitwise operations:</p>
- <div style="margin-left: 40px;" class="fragment">
- <pre class="fragment">x, y, z, t, q : BITVECTOR(1024);<br><br>ASSERT(x=~x);<br>ASSERT(x&y&t&z&q = x);<br>ASSERT(x|y = t);<br>ASSERT(BVXOR(x,~x)=t);<br>QUERY(FALSE);<br></pre>
- </div>
- <p style="margin-left: 40px;"><span style="font-weight: bold;">Example
-4</span>
-illustrates the use of predicates and all the arithmetic
-operations:</p>
- <div style="margin-left: 40px;" class="fragment">
- <pre class="fragment">x, y : BITVECTOR(4);<br><br>ASSERT(x=0hex5);<br>ASSERT(y = 0bin0101);<br>QUERY(<br>BVMULT(8,x,y)=BVMULT(8,y,x)<br>AND<br>NOT(BVLT(x,y))<br>AND<br>BVLE(BVSUB(8,x,y), BVPLUS(8, x, BVUMINUS(x)))<br>AND <br>x = BVSUB(4, BVUMINUS(x), BVPLUS(4, x,0hex1))<br>);<br></pre>
- </div>
- <p style="margin-left: 40px;"><span style="font-weight: bold;">Example
-5</span>
-illustrates the use of shift functions</p>
- <div class="fragment">
- <pre style="margin-left: 40px;" class="fragment">x, y : BITVECTOR(8);<br>z, t : BITVECTOR(12);<br><br>ASSERT(x=0hexff);<br>ASSERT(z=0hexff0);<br>QUERY(z = x << 4);<br>QUERY((z >> 4)[7:0] = x);<br><br></pre>
- </div>
- <p>For invalid inputs, the COUNTEREXAMPLE command can be used to
-generate
-appropriate counterexamples. The generated counter example is
-essentially a bitwise assignment to the variables in the input.</p>
- <div style="margin-left: 40px;"> </div>
- </td>
- </tr>
- </tbody>
-</table>
-<a href="#stp"></a><br>
-</body>
-</html>
+++ /dev/null
-<!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>
+++ /dev/null
-<!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>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>
- <br>
- </td>
- <td style="vertical-align: top;">
- <h2> <span style="color: rgb(255, 102, 0);">Download</span> </h2>
- <ul>
- <li> <a href="stp.tar.gz">STP </a> (accepts CVCL format)
-:
-Linux binary and library (last updated April 25, 2007) </li>
- <li> <a href="stp.smt">STP.smt</a> (accepts SMT format)
-:
-Linux binary </li>
- <li> The <a href="c_interface.h">c_interface.h</a> file </li>
- <li> The <a href="cinterface.tar.gz">c_interface testcases</a>
-file </li>
- <li> WARNING: PLEASE DO `ulimit -s unlimited` BEFORE RUNNING
-STP.
-OTHERWISE, THE YACC PARSER WILL SEGFAULT ON BIG EXAMPLES</li>
- </ul>
- <h2 style="color: rgb(255, 102, 0);">STP Examples</h2>
- <div style="margin-left: 40px;">These <a
- href="http://chicory.stanford.edu/STP/cav2007-examples.tar.gz">examples</a>
-were used for the CAV 2007 paper<br>
- </div>
- <h2><span style="color: rgb(255, 102, 0);">Authors</span><br>
- </h2>
-Vijay Ganesh and David L. Dill<br>
- <a style="font-weight: bold;" href="stp.html#stp"></a>
- <div style="margin-left: 40px;"> </div>
- </td>
- </tr>
- </tbody>
-</table>
-<a href="#stp"></a><br>
-</body>
-</html>
projects / francis / stp.git / commitdiff