...
Also see the main CRASH project web page.
| HTML |
|---|
<a <p class="topbutton"><a href="http://www.nuprl.org/crash/default.php" class="submenulink" ><span class="topbuttonframe">CRASH home</span></a> <span class="topbuttonframe"><a href="introextended.php" class="submenulink" >About CRASH</a></span> <span class="topbuttonframe"><a href="http://confluence.cornell.edu/display/prl/Correct-by-Construction+Methodology" class="submenulink" >Methodology</a></span> <span class="topbuttonframe"><a href="../software" class="submenulink">Software</a></span> <span class="topbuttonframe"><a href="people.php" class="submenulink" >People</a></span> <span class="topbuttonframe"><a href="publications.php" class="submenulink" >Publications</a></span></span>p> |
Background
Our method uses formal proofs of high-level system requirements then to synthesize code from the proven specification. Within our work on distributed systems we use the following concepts:
...