📄 http:^^www.cs.utexas.edu^users^psp^

📁 This data set contains WWW-pages collected from computer science departments of various universities
💻 EDU^USERS^PSP^
字号:
MIME-Version: 1.0
Server: CERN/3.0
Date: Monday, 06-Jan-97 19:47:00 GMT
Content-Type: text/html
Content-Length: 5239
Last-Modified: Monday, 25-Nov-96 19:47:27 GMT

<html><!-- Changed by: Rajeev Joshi, 17-Jul-1996 --><!-- Changed by: Jacob Kornerup, 24-Oct-1996 --><!-- Changed by: Rajeev Joshi, 25-Nov-1996 --><head><title>PSP group at UT Austin</title></head><body><h1>PSP Group at UT Austin</h1>This is the home page for the PSP group in the <!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><ahref="http://www.cs.utexas.edu/">Department of Computer Sciences</a> at <!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><ahref="http://wwwhost.cc.utexas.edu/">The University of Texas atAustin</a>. PSP stands for Programs,Specifications and Proofs.  The emphasis of the work of our group is to deriveparallel and distributed programs in a rigorous manner. The group issupervised by <!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><a href="http://www.cs.utexas.edu/users/misra">Jayadev Misra</a>, who developed the theories we work on. The research areas are: <!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><a href="#unitysec">UNITY</a>,<!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><a href="#plistsec">Powerlists</a> and <!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><a href="#seusssec">Seuss</a>. <p>Current and former members of the groupinclude:<ul><li> <!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><a href="http://www.cs.utexas.edu/users/misra/">Jayadev Misra</a><li> Will Adams<li> <!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><a href="http://www.cs.utexas.edu/users/carruth/">Al Carruth</a><li> <!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><a href="ftp://ftp.bellcore.com/pub/ernie/research/homepage.html">Ernie Cohen</a>  (<em>graduated 1992</em>)<li> Rajeev Joshi<li> <!WA9><!WA9><!WA9><!WA9><!WA9><!WA9><!WA9><!WA9><!WA9><!WA9><!WA9><!WA9><!WA9><!WA9><!WA9><!WA9><!WA9><a href="http://www.cs.utexas.edu/users/markus/">Markus Kaltenbach</a> (<em>graduated 1996</em>)<li> Edgar Knapp (<em>graduated 1992</em>)<li> <!WA10><!WA10><!WA10><!WA10><!WA10><!WA10><!WA10><!WA10><!WA10><!WA10><!WA10><!WA10><!WA10><!WA10><!WA10><!WA10><!WA10><a href="http://www.cs.utexas.edu/users/kornerup/">Jacob Kornerup</a><li> <!WA11><!WA11><!WA11><!WA11><!WA11><!WA11><!WA11><!WA11><!WA11><!WA11><!WA11><!WA11><!WA11><!WA11><!WA11><!WA11><!WA11><a href="http://www.cs.utexas.edu/users/kruegeri/">Ingolf Kr&uuml;ger</a> (<em>graduated 1996</em>)<li> Josyula R Rao (<em>graduated 1992</em>)<li> <!WA12><!WA12><!WA12><!WA12><!WA12><!WA12><!WA12><!WA12><!WA12><!WA12><!WA12><!WA12><!WA12><!WA12><!WA12><!WA12><!WA12><a href="http://www.bell-labs.com/~markstas/">Mark Staskauskas</a> (<em>graduated 1992</em>)</ul><hr><p><h1>Publications</h1>Below we summarize the areas we work in; wherever possible we give links topapers that are available electronically. <p><h2> <a name="unitysec">UNITY</a> </h2>UNITY is a programming notation and a logic to reason about parallel anddistributed programs. Unity is presented in the book: J. Misra and K.M. Chandy, <i>Parallel Program Design: A Foundation</i>,Addison-Wesley, 1988. <p>The <!WA13><!WA13><!WA13><!WA13><!WA13><!WA13><!WA13><!WA13><!WA13><!WA13><!WA13><!WA13><!WA13><!WA13><!WA13><!WA13><!WA13><a href="http://www.cs.utexas.edu/users/psp/notesunity.html">notes on UNITY</a> is a series ofpapers presenting various results about UNITY and its applications. Thenotes assumes a basic understanding of the UNITY theory as presented inChandy and Misra's book. <p>Since the publication of the book several improvements have been made inthe theory, some of which are reflected in the <!WA14><!WA14><!WA14><!WA14><!WA14><!WA14><!WA14><!WA14><!WA14><!WA14><!WA14><!WA14><!WA14><!WA14><!WA14><!WA14><!WA14><ahref="http://www.cs.utexas.edu/users/psp/notesunity.html">notes on UNITY</a>, Jayadev Misra has written amanuscript for a book that presents the <!WA15><!WA15><!WA15><!WA15><!WA15><!WA15><!WA15><!WA15><!WA15><!WA15><!WA15><!WA15><!WA15><!WA15><!WA15><!WA15><!WA15><a href="http://www.cs.utexas.edu/users/psp/newunity.html">NewUNITY</a>, this includes the introduction of a new temporal operator<em>co</em> for specifying safety.<p>See <!WA16><!WA16><!WA16><!WA16><!WA16><!WA16><!WA16><!WA16><!WA16><!WA16><!WA16><!WA16><!WA16><!WA16><!WA16><!WA16><!WA16><a href="http://www.cs.utexas.edu/users/psp/unity.html">further UNITY references</a> forreferences to other papers and implementations.<p><!WA17><!WA17><!WA17><!WA17><!WA17><!WA17><!WA17><!WA17><!WA17><!WA17><!WA17><!WA17><!WA17><!WA17><!WA17><!WA17><!WA17><a href="http://www.cs.utexas.edu/users/markus/">Markus Kaltenbach</a> is currently writing asymbolic model checker</a> forfinite state UNITY programs, called the <!WA18><!WA18><!WA18><!WA18><!WA18><!WA18><!WA18><!WA18><!WA18><!WA18><!WA18><!WA18><!WA18><!WA18><!WA18><!WA18><!WA18><a href="http://www.cs.utexas.edu/users/markus/uv/uv.html">UNITYVerifier (UV)</a>.<p><!WA19><!WA19><!WA19><!WA19><!WA19><!WA19><!WA19><!WA19><!WA19><!WA19><!WA19><!WA19><!WA19><!WA19><!WA19><!WA19><!WA19><a href="http://www.cs.utexas.edu/users/carruth/">Al Carruth</a> has extended the UNITY logic toinclude real time aspects of computing and hybrid systems.<h2> <a name="plistsec">Powerlists</a> </h2>Powerlists is a notation for synchronous parallel programs and circuits.The data structure is a list of length equal to a power of two, with twodifferent operations for balanced divisions of lists. Many parallelalgorithms have a succinct presentation  and simple proofs in thepowerlist notation. Jayadev Misra's paper <!WA20><!WA20><!WA20><!WA20><!WA20><!WA20><!WA20><!WA20><!WA20><!WA20><!WA20><!WA20><!WA20><!WA20><!WA20><!WA20><!WA20><ahref="ftp://ftp.cs.utexas.edu/pub/psp/powerlist/misra.1.ps.Z">Powerlists:A Structure for Parallel Recursion</a> presents the notation and givesnumerous examples of algorithms and proofs of their correctness,including the Fast Fourier Transform and Batcher's sorting network.<p>Will Adams has studied how different arithmetic circuits, such asadders and multipliers, can be specified and proved correct in thepowerlist notation. His paper <!WA21><!WA21><!WA21><!WA21><!WA21><!WA21><!WA21><!WA21><!WA21><!WA21><!WA21><!WA21><!WA21><!WA21><!WA21><!WA21><!WA21><ahref="ftp://ftp.cs.utexas.edu/pub/techreports/tr94-02.ps.Z">Verifying addercircuits using powerlists</a> is available.<p><!WA22><!WA22><!WA22><!WA22><!WA22><!WA22><!WA22><!WA22><!WA22><!WA22><!WA22><!WA22><!WA22><!WA22><!WA22><!WA22><!WA22><a href="http://www.cs.utexas.edu/users/kornerup">Jacob Kornerup</a> has studied how powerlist programscan be mapped efficiently to different parallel architectures, speciallyhypercubes.  See his <!WA23><!WA23><!WA23><!WA23><!WA23><!WA23><!WA23><!WA23><!WA23><!WA23><!WA23><!WA23><!WA23><!WA23><!WA23><!WA23><!WA23><a href="http://www.cs.utexas.edu/users/kornerup/kornerup-papers.html">List ofpapers</a> for details.<h2> <a name="seusssec">Seuss</a> </h2>Seuss is an offspring of the work on UNITY. It addresses the issue ofprogram composition, by restricting how program components caninterfere with each other. For an introduction to Seuss, read the <!WA24><!WA24><!WA24><!WA24><!WA24><!WA24><!WA24><!WA24><!WA24><!WA24><!WA24><!WA24><!WA24><!WA24><!WA24><!WA24><!WA24><ahref="http://www.cs.utexas.edu/users/psp/seuss-overview.html">Overview of Seuss</a>.  A few chapters froma monograph <!WA25><!WA25><!WA25><!WA25><!WA25><!WA25><!WA25><!WA25><!WA25><!WA25><!WA25><!WA25><!WA25><!WA25><!WA25><!WA25><!WA25><ahref="ftp://ftp.cs.utexas.edu/pub/psp/seuss/discipline.ps.Z">ADiscipline of Multiprogramming</a> written by Jayadev Misra are alsoavailable. A compiler for Seuss that genrates C++ code and PVM callsfor message communicating networks is described in the thesis <!WA26><!WA26><!WA26><!WA26><!WA26><!WA26><!WA26><!WA26><!WA26><!WA26><!WA26><!WA26><!WA26><!WA26><!WA26><!WA26><!WA26><ahref="http://www.cs.utexas.edu/users/kruegeri/Thesis.ps.Z">Anexperiment in compiler design for a concurrent object-basedprogramming language</a> of <!WA27><!WA27><!WA27><!WA27><!WA27><!WA27><!WA27><!WA27><!WA27><!WA27><!WA27><!WA27><!WA27><!WA27><!WA27><!WA27><!WA27><a href="http://www.cs.utexas.edu/users/kruegeri/">IngolfKr&uuml;ger</a>.<h2> FTP site </h2>Many of the above papers can be found in the<!WA28><!WA28><!WA28><!WA28><!WA28><!WA28><!WA28><!WA28><!WA28><!WA28><!WA28><!WA28><!WA28><!WA28><!WA28><!WA28><!WA28><a href="ftp://ftp.cs.utexas.edu/pub/psp/">PSP ftp-site</a></ol><hr><address><!WA29><!WA29><!WA29><!WA29><!WA29><!WA29><!WA29><!WA29><!WA29><!WA29><!WA29><!WA29><!WA29><!WA29><!WA29><!WA29><!WA29><a href="mailto:kornerup@cs.utexas.edu">Jacob Kornerup</a></address></body></html>
⌨️ 快捷键说明

复制代码 Ctrl + C
搜索代码 Ctrl + F
全屏模式 F11
切换主题 Ctrl + Shift + D
显示快捷键 ?
增大字号 Ctrl + =
减小字号 Ctrl + -