☆ Linking STeP with SPIN ☆ <title> <base href="http://www.cs.stanford.edu/~tingz/"> </head> <div class=content> <h1>Linking STeP with SPIN <br><br> <a href="http://www.informatik.uni-trier.de/~ley/db/indices/a-tree/b/Browne:Anca.html"><font style="font-size: 14px;">Anca Browne</font></a>, <a href="http://theory.stanford.edu/~sipma"><font style="font-size: 14px;">Henny B. Sipma</font></a>, <a href=""><font style="font-size: 14px;">Ting Zhang</font></a> </h1> <br><br> <div class=page> <a name="abstract"></a> <h2>Abstract</h2> <P><BR>We have connected STeP, the Stanford Temporal Prover, with SPIN, an LTL model checker. In this paper we describe the translation of fair transition systems into Promela, in particular how weak and strong fairness constraints are handled. The paper presents some preliminary experimental results using this connection. <br><br> </div> <div class=page> <a name="download"></a> <h2>Download</h2> <br>Talk: <A href="papers/spin00/spin00.ps"><img border="0" src="//gif/ps.gif"></A> <A href="papers/spin00/spin00.pdf"><img border="0" src="//png/pdf.png"></A> </div>  <div class="footer"> <a href="index.html">Home</a> <a href="papers/papers_by_category.html">By Category</a> <a href="papers/papers_by_year.html">By Year</a> <a href="papers/papers_by_topic.html">By Topic</a> </div> </body> </html>