http:^^www.cs.cornell.edu^info^people^tah^formal_methods_at_cornell.html

来自「This data set contains WWW-pages collect」· HTML 代码 · 共 74 行

MIME-Version: 1.0
Server: CERN/3.0
Date: Sunday, 24-Nov-96 21:26:43 GMT
Content-Type: text/html
Content-Length: 2228
Last-Modified: Thursday, 12-Oct-95 01:54:35 GMT


<title>Formal Methods at Cornell</title>
<h1>Formal Methods at Cornell</h1>
<i>Cornell University<br>
Ithaca, NY 14853</i>
<h2>Faculty</h2>
<ul>
<li><b><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><a href="http://www.cs.cornell.edu/Info/Faculty/Bard_Bloom.html">
Bard Bloom</a></b>
(<i>[e-mail]</i>):
semantics of programming languages, distributed algorithms
<p>
<li><b><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><a href="http://www.cs.cornell.edu/Info/Faculty/Robert_Constable.html">
Robert L. Constable</a></b>
(<i>[e-mail]</i>):
theory of computation, programming logics, automated reasoning
<p>
<li><b><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><a href="http://www.cs.cornell.edu/Info/People/gries/gries.html">
David Gries</a></b>
(<i>[e-mail]</i>):
programming methodology, programming languages, compiler construction
<p>
<li><b><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><a href="http://www.cs.cornell.edu/Info/People/tah/tah.html">
Thomas A. Henzinger</a></b>
(<i>[e-mail]</i>):
formal support for the development and analysis of concurrent, real-time,
and embedded systems
<p>
<li><b><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><a href="http://www.cs.cornell.edu/Info/People/kozen/kozen.html">
Dexter Kozen</a></b>
(<i>[e-mail]</i>):
theory of computation, computational complexity, programming logics,
semantics
<p>
<li><b><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><a href="http://orac.ee.cornell.edu:8080/~linder/leeser.html">
Miriam Leeser</a></b>
(<i>[e-mail]</i>):
application of formal methods to hardware verification and synthesis
<p>
<li><b>
Anil Nerode</b>
(<i>[e-mail]</i>):
game methods for extracting correct concurrent programs, 
relaxed variational methods for extracting correct digital control
programs for continuous plants
<p>
<li><b><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><a href="http://www.cs.cornell.edu/Info/Faculty/Fred_Schneider.html">
Fred B. Schneider</a></b>
(<i>[e-mail]</i>):
concurrent programming, particularly for fault-tolerant, real-time, and 
distributed systems
</ul>
<h2>Projects</h2>
<ul>
<li><b><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><a href="http://www.cs.cornell.edu/Info/People/tah/hytech.html">
HyTech</a></b>
(<i>[e-mail]</i>):
a symbolic model checker for linear hybrid systems
<p>
<li><b><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><a href="http://www.cs.cornell.edu/Info/Projects/NuPrl/nuprl.html">
NuPrl</a></b>
(<i>[e-mail]</i>):
an interactive proof development system
</ul>
<i>Last updated on September 18, 1994.<br>
[e-mail]</i>