📄 gerard.html
字号:
<html>
<body bgcolor="#FFFFFF" TEXT="#000000" LINK="#0000FF" VLINK="#330088" ALINK="#FF0044">
<title>Gerard J. Holzmann</title>
<!-- BELL-LABS
category user
username Holzmann, Gerard
contact gerard@bell-labs.com
-->
<img src=holzmann.gif>
<font face="verdana, arial, helvetica">
<h2>Gerard J. Holzmann</h2>
<h3>gerard@research.bell-labs.com</h3>
</font>
Member of the Computing Principles Research Department at Bell Labs
in Murray Hill, NJ.
Interested in formal verification, model checking,
requirements capture and analysis, early fault detection,
testing, tool design, graphical user interfaces, technology transfer,
history.
<br>
<br>
<table cols=2>
<tr>
<td valign=top width=80>
<font face="verdana, arial, helvetica">
<h2>Software</h2>
</td>
<td valign=middle>
<ul>
<li><a href="http://netlib.bell-labs.com/netlib/spin/whatispin.html"><b>spin</b></a>
an efficient LTL model checker for distributed systems software (a design
verification system), distributed with
<a href="http://netlib.bell-labs.com/netlib/spin/index.html">source</a>.
<li><a href="micro.html"><b>microtrace</b></a> a demo
awk-script for FSM verification (written 1987).
<li><a href="http://netlib.bell-labs.com/netlib/popi/index.html"><b>pico/popi</b></a>
digital darkroom software (written 1984), with <a href="http://netlib.bell-labs.com/netlib/popi/index.html">source</a>.
<li><a href="http://cm.bell-labs.com/cm/cs/what/ubet/"><b>msc, poga</b></a> prototype tools from around 1995 for early fault detection, currently being productized
within Lucent as the uBET tool.
<li><b>sdlvalid</b>, an early verifier for SDL.
we wrote the tool in 1987/1988, and it was used internally for about five years.
it was never approved for public release.
<li><b>feaver</b> is a software model checking system based on <b>spin</b> and used to verify
properties of Lucent's
<a href="http://www.lucent.com/dms/products/pas_c.html">PathStar (r)</a>
access server.
our system mechanically extracts a formal model from
unedited C code, and verifies it against a large library of
logic properties.
the checks are executed on dedicated multi-processing hardware (called
<b>trailblazer</b>) with the equivalent of 8 GigaHertz of processing power.
(more detail on this project in the abstracts.)
</ul>
</td>
</tr>
<tr>
<td valign=top width=80>
<font face="verdana, arial, helvetica">
<h2>Books</h2>
</td>
<td valign=middle>
<ul>
<li><a href="/cm/cs/who/gerard/popd.html">Design and Validation of Computer Protocols</a>, Prentice Hall, 1991</li>
<li><a href="/cm/cs/who/gerard/hist.html">The Early History of Data Networks</a>, IEEE Computer Society Press, 1995</li>
<li><a href="/cm/cs/who/gerard/popi.html">Beyond Photography -- The Digital Darkroom</a>, Prentice Hall, 1988</li>
</ul>
</td>
</tr>
<tr>
<td valign=top width=80>
<font face="verdana, arial, helvetica">
<h2>Papers etc.</h2>
</td>
<td valign=middle>
<ul>
<li><a href="abs.html">some abstracts (with postscript for selected papers)</a></li>
<li>publications (<a href="/cm/cs/bib/gerard.bib">bibtex format</a>
or <a href="/cm/cs/bib2html/gerard.html">html format</a>)</li>
<li><a href="http://www.fee.uwaterloo.ca/~sleue/6thSPIN99.html">program for the 6th Spin workshop</a>, September 1999, Toulouse, France</li>
<li>index of Spin <a href="http://netlib.bell-labs.com/netlib/spin/news.html">newsletters.</a></li>
<li>colleagues in our Bell Labs <a href="/cm/cs/what/formal_methods/">
formal methods group</a>.
</ul>
</td>
</tr>
<tr>
<td valign=top width=80>
<font face="verdana, arial, helvetica">
<h2>Little Movies</h2>
</td>
<td valign=middle>
<ul>
<li> <b>pixelface</b>, 1988, a five minute demo of Pico/Popi.
<br>
A portion of the video was shown on CNN Science &
Technology report in 1989.
<li> <b>walkman</b>, 1984, with Rob Pike, Don Mitchell, and Lillian Schwartz.
<br>
A frame from the movie was used for the cover of IEEE Spectrum,
June 1984.</li>
</ul>
</td>
</tr>
<tr>
<td valign=top width=80>
<font face="verdana, arial, helvetica">
<h2>Covers etc.</h2>
</td>
<td valign=middle>
<ul>
<li> <a href="../../logo.246x121.jpg">CS Research Center logo,</a> 1997.
<br>
<li> <a href="inferno.jpg">original Inferno logo,</a> 1996.
<br>
<li> <a href="/plan9/distrib.html">CD, floppies, and manual covers, Plan-9, 2nd Edition,</a>
<br>
Pub. Harcourt Brace & Company, Orlando, Fl., 1995.
<br>
(Illustrations from Louis Figuier, Les Merveilles de la Science, Paris 1867.)</li>
<li> <a href="holzmann-p9v1.gif">CD, Plan-9 from Bell Labs, 1st Edition,</a> 1992.
<br>
(Three actors from Plan-9, the movie by Ed Wood.)</li>
<li> <a href="holzmann-chess.gif">CD, Chess Endgames, Vols 1-4,</a> (issued by Ken Thompson, 1991)
<br>
(Chess-piece and a small part of Leonardo da Vinci's Creation.)</li>
<li> <a href="holzmann-atttj.gif">AT&T Technical Journal,</a> March/April 1987,
Vol 66, Issue 2.
<br>
(Cover with a transformed Pico/Popi Image of Peter Weinberger's portrait.)</li>
<li> <a href="holzmann-bstj.gif">AT&T Bell Laboratories Technical Journal,</a> October 1984,
Vol 63, No. 8, Part 2.
<br>
Special Issue on Unix (cover with computer generated graphics.)</li>
</ul>
</td>
</tr>
</table>
<font face="verdana, arial, helvetica">
<dl>
<dt><em>Address:</em>
<dd>Gerard J. Holzmann
<dd>Bell Laboratories, MH 2C-521
<dd>700 Mountain Avenue
<dd>Murray Hill, New Jersey 07974
<dd>U.S.A.
<dd>908-582-6335 <em>(phone)</em>
<dd>908-582-5857 <em>(fax)</em>
</dl>
</body>
</html>
⌨️ 快捷键说明
复制代码
Ctrl + C
搜索代码
Ctrl + F
全屏模式
F11
切换主题
Ctrl + Shift + D
显示快捷键
?
增大字号
Ctrl + =
减小字号
Ctrl + -