?? http:^^www.cs.cornell.edu^info^department^annual95^faculty^schneider.html
字號:
MIME-Version: 1.0
Server: CERN/3.0
Date: Wednesday, 20-Nov-96 18:57:15 GMT
Content-Type: text/html
Content-Length: 9558
Last-Modified: Thursday, 30-Nov-95 21:21:19 GMT
<html><head><title>Fred B. Schneider</title></head><body><!WA0><!WA0><!WA0><!WA0><a href="http://www.cs.cornell.edu/Info/People/fbs/fbs.gif"><!WA1><!WA1><!WA1><!WA1><img align=left vspace=3 hspace=15 src="http://www.cs.cornell.edu/Info/People/fbs/fbs-thumb.gif"></a><h2>Fred B. Schneider <br>Professor<br>PhD State Univ. of N.Y., Stony Brook, 1978</h2><p><hr><p>Techniques for understanding concurrent programs are becoming increasingly important as distributed computing systems become widespread in mission-critical applications. My research has focused on the development of these techniques.<p>I have been heavily involved in applying assertional reasoning to the design of concurrent, distributed, fault-tolerant, and real-time programs. I am completing a textbook on this subject. Along with David Gries, I continue investigations concerning our first-order equational logic E. This past year, we streamlined the inference rules and evaluated a number of techniques for handling undefined terms and partial functions.<p>Thomas Bressoud and I completed building and analyzing our hypervisor-based implementation of replication management for HP's PA-RISC architecture. Our protocols ensure that the sequence of instructions executed by two virtual machines running on different physical processors are identical. The protocols also coordinate I/O issued by these virtual machines. Use of a hypervisor to implement replica coordination is attractive - at least, in theory. When replica coordination is implemented in a hypervisor, it instantly becomes available to all hardware realizations of the given instruction-set architecture, including realizations that did not exist when the hypervisor was written. Second, when replica coordination is implemented in a hypervisor, a single implementation suffices for every operating system that executes on that instruction-set architecture. Finally, by implementing replica coordination in a hypervisor, the applications programmer is freed from this task.<p>Jointly with Dag Johansen (University of Tromsø, Norway) and Robbert van Renesse, I started the TACOMA project (Tromsø And COrnell Moving Agents) to investigate support and use of mobile processes in building mission-critical applications. By structuring a system in terms of agents, applications can be constructed in which communication-network bandwidth is conserved. Data may be accessed only by an agent executing at the same site as the data resides. An agent typically will filter or otherwise reduce the data it reads, carrying with it only the relevant information as it roams the network. Two TACOMA prototypes have been completed, and we are implementing a third system based on our experiences.<p>Finally, I developed with Scott Stoller a new algorithm for detecting whether a particular computation of an asynchronous distributed system could have passed through a global state satisfying some given state predicate. The new algorithm allows more efficient detection than is possible with previous algorithms.<p><hr><H2>University Activities</H2><ul><li>Sabbatical leave, 1994-95</ul><H2>Professional Activities</H2><ul><li>Editor-in-chief, <EM>Distributed Computing</EM><li>Editor, <EM>Information Processing Letters</EM><li>Editor, <EM>IEEE Transactions on Software Engineering</EM><li>Editor, <EM>High Integrity Systems</EM><li>Editor, <EM>Annals of Software Engineering</EM><li>Editor, <EM>ACM Computing Surveys</EM><li>Co-Editor, Texts and Monographs in Computer Science, Springer-Verlag<li>Program Committee Member, 3rd International School and Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems<li>Program Committee Member, 3rd International Conference on the Mathematics of Program Construction<li>Program Committee Member, 4th International Workshop On Responsive Computer Systems<li>Program Committee Member, Workshop on Composability of Fault-resilient Real-Time Systems<li>Program Committee Member, Fifth IFIP Working Conference on Dependable Computing for Critical Applications<li>Program Committee Member, Sixteenth IEEE International Real-Time Systems Symposium<li>Program Committee Member, DIMACS Workshop on Verification and Control of Hybrid Systems<li>Steering committee, Center for High Integrity Software Systems Assurance (CHISSA), National Institute of Standards and Technology<li>Member, ISAT Defensive Information Warfare Study Group, Advanced Research Projects Agency<li>Review committee, Leibniz Center at Hebrew University<li>Member, IFIP Working Group 2.3 (Programming Methodology)</ul><H2>Awards</H2><ul><li>Fellow, American Association for Advancement of Science<li>Fellow, Association for Computing Machinery</ul><H2>Lectures</H2><ul><li>Proof outlines for programs. 6 lectures. 15th International Summer School, Marktoberdorf, Germany, July 1994.<li>On the origin of traditions. Banquet speech. 15th International Summer School, Marktoberdorf, Germany, July 1994.<li>Reasoning about programs by exploiting the environment. AFOSR Grantees/Contractors Meeting In Software and Systems, Washington, D.C., Sept. 1994.<li>Verifying hybrid systems by exploiting the environment. Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems. Lubeck, Germany, Sept. 1994.<li>Panelist: comparative merits of synchronous, partially synchronous, and asynchronous models for safety-critical real-time systems. Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems. Lubeck, Germany, Sept. 1994.<li>Moderator: issues in writing formal specifications. Specification and Refinement of Reactive Systems. International Conference and Research Center for Computer Science, Dagstuhl, Germany, Sept. 1994.<li>Merging policies. Workshop on Computer Support for Policy Analysis and Design. George Mason University, Virginia, Dec. 1994.<li>Avoiding AAS mistakes. Invited speaker. Air Traffic Management Workshop, NASA Ames Research Center, Feb. 1995.<li>Reasoning about programs by exploiting the environment. Technical University of Munich. Munich, Germany, Feb. 1995.<li>Proof outlines of the past. University of North Carolina, Chapel Hill, North Carolina, March 1995.<li>Adding fault-tolerance, virtually. Distinguished Lecture Series, University of North Carolina, Chapel Hill, North Carolina, March 1995.<li>Moderator and panel organizer: teaching logic as tool. SIGCSE Technical Symposium on Computer Science Education, Nashville, Tennessee, March 1995.<li>Proof outlines of the past. Technion, Haifa, Israel, March 1995.<li>Adding fault-tolerance, virtually. University of Tromsø, Tromsø, Norway, April 1995.<li>Concurrent programs from specifications. University of Tromsø, Tromsø, Norway, April 1995.<li>Placing agents on airplanes - a view of AAS and its successor. ARPA ISAT Defensive Information Warfare Study Group Meeting, Washington, D.C., June 1995.</ul><H2>Publications</H2><ul><li>Reasoning about programs by exploiting the environment. <EM>Proceedings 21st International Colloquium, ICALP'94</EM> (Jerusalem, Israel, July 1994), <EM>Lecture Notes in Computer Science 820,</EM> Springer-Verlag, New York, 328-339 (with L. Fix).<li>Notes on proof outline logic. Working Material. 15th International Summer School, Marktoberdorf, Germany, July 1994.<li>Research on fault-tolerant and real-time computing. Software and Systems Program Summary. (Bolling Air Force Base, Washington D.C., Sept. 1994), Air Force Office of Scientific Research, 75-77.<li>Hybrid verification by exploiting the environment. <EM>Formal Techniques in Real-Time and Fault-Tolerant Systems</EM> (Lubeck, Germany, September 1994), <EM>Lecture Notes in Computer Science, Volume 863,</EM> Springer-Verlag, New York, 1-18 (with Limor Fix).<li>Equational propositional logic. <EM>Information Processing Letters 53,</EM> 3 (February 1995), 145-152 (with D. Gries).<li>Refinement for fault-tolerance: An aircraft hand-off protocol. <EM>Foundations of Ultradependable Parallel and Distributed Computing, Paradigms for Dependable Applications,</EM> Kluwer Academic Publishers, 1994, 39-54 (with K. Marzullo and J. Dehn).<li>Teaching logic as a tool. <EM>Proceedings 26th SIGCSE Technical Symposium on Computer Science Education</EM> (Nashville, Tennessee, March 1995), <EM>SIGCSE Bulletin 27,</EM> 1, 384-385 (with D. Gries).<li>Operating system support for mobile agents. <EM>Proceedings Fifth Workshop on Hot Topics in Operating Systems HOTOS-V</EM> (Orcas Island, Washington, May 1995), 42-45 (with Dag Johansen and Robbert van Renesse).<li>Verifying programs that use causally-ordered message-passing. <EM>Science of Computer Programming 24,</EM> 2 (1995), 105-128 (with S. Stoller).<li>On teaching proof. <EM>Arts & Sciences NewsLetter 16,</EM> 2 (Spring 1995), 3 (with D. Gries).<li>A new approach to discrete teaching mathematics. <EM>Primus V,</EM> 2 (June 1995), 113-138 (with D. Gries).</ul><p><hr>Return to: <dl><dt><!WA2><!WA2><!WA2><!WA2><IMG SRC="http://www.cs.cornell.edu/Icons/redball.gif"> <!WA3><!WA3><!WA3><!WA3><a href="http://www.cs.cornell.edu/Info/Department/Annual95/Beginning/annual-rpt95-home.html"> 1994-1995 Annual Report Home Page</a><dt><!WA4><!WA4><!WA4><!WA4><IMG SRC="http://www.cs.cornell.edu/Icons/redball.gif"> <!WA5><!WA5><!WA5><!WA5><a href="http://www.cs.cornell.edu/"> Departmental Home Page</a><p>If you have questions or comments please contact:<!WA6><!WA6><!WA6><!WA6><a href="mailto:www@cs.cornell.edu">www@cs.cornell.edu.</a><p><hr>Last modified: 24 November 1995 by Denise Moore (denise@cs.cornell.edu).</body></html>?? 快捷鍵說明
復制代碼
Ctrl + C
搜索代碼
Ctrl + F
全屏模式
F11
切換主題
Ctrl + Shift + D
顯示快捷鍵
?
增大字號
Ctrl + =
減小字號
Ctrl + -