[an error occurred while processing this directive]<title>Department of Computer Science: Concurrency</title>
<meta name="keywords"
      content="Department of Computer Science Research Activities Concurrency"></meta>
<meta property="og:site_name" content="Department of Computer Science"></meta>
<meta property="og:title" content="Concurrency"></meta>
<meta property="og:image"
      content="http://www.cs.ox.ac.uk/images/CompSci_logo_landscapeL_rgb_corrected.jpg"></meta>
<meta property="og:url" content="http://www.cs.ox.ac.uk/activities/concurrency/"></meta>
<meta name="Author" content="Tom Newcomb, Tomasz Mazur"/>
[an error occurred while processing this directive]
<div id="breadcrumb">
   <span id="breadcrumb-label">You are here:</span>
   <ul>
      <li>
         <a href="/">Home</a>
      </li>
      <li>
         <a href="/research/">Research</a>
      </li>
      <li>
         <a href="/research/activities.html">Activities</a>
      </li>
      <li>
         <a href="/activities/concurrency">Concurrency</a>
      </li>
       <li>
         <a href="/activities/concurrency/tools">Tools</a>
      </li>
      <li>
         <span class="youarehere">FDR</span>
      </li>
   </ul>
</div>
<div id="content">

<h1>
FDR</h1>
<div class="personalContent">
The chief proof and analytic tool for CSP at present is called FDR
(standing
for Failures/Divergences Refinement). FDR is a model checking tool
which allows the verification of a wide
range of correctness conditions, including deadlock and livelock
freedom
as well as general safety and liveness properties. When these
conditions
are not satisfied, the reasons can be investigated.
<br>
<br>
<br>
Related publications<br>
1. Formal Systems (Europe) Ltd., Failures-Divergences Refinement - FDR2
User Manual, 1999. (<a
 href="http://www.fsel.com/documentation/fdr2/fdr2manual.pdf">PDF</a>)<br>
2. A. W. Roscoe, The theory and practice of concurrency (Appendix C -
The operation of FDR), Prentice Hall, 1998. (<a
 href="http://www.cs.ox.ac.uk/people/bill.roscoe/publications/68b.pdf">PDF</a>)
<p class="publicationDetails"><br>
</p>
<h3>
links
</h3>
<p><a href="http://www.fsel.com/software.html">FDR download page</a>
<a href="http://www.fsel.com/"><br>
</a></p>
</div>

</div>
[an error occurred while processing this directive]
[an error occurred while processing this directive]
[an error occurred while processing this directive]