Gerard J. Holzmann

Gerard J. Holzmann

gholzmann [insert atsign here] acm.org

NASA/JPL Laboratory for Reliable Software,
and Caltech CS, Pasadena, CA.

interested in: software reliability, software analysis methods, formal verification, metrics, logic model checking, distributed systems design, analysis of multi-threaded software, testing, requirements capture and analysis, algorithms, user interface design, graphic design, text processing, image processing, history of technology, technology transfer.

before joining jpl i worked in the cs research group at bell labs (1980-1981 and 1983-2003) a truly remarkable group that was given virtually complete freedom to pursue research goals, with no perceptible management oversight. i made a map of the 5th floor at stair 9 in building 2, the most desirable location for one's office at the time. the map lists the main occupants for each office over the years, with the person that occupied it the longest in red. from the 30-some people shown on this map, just a few remained to witness the final disappearance of center 1127 from the bell labs org charts in august 2005: rae mclellan, howard trickey (since moved to google) and dennis ritchie. one by one, the others all found a safe haven elsewhere.
remarkably, 8 of the 30 people whose name is shown on this map (and about 18 former members of center 1127 alltogether) now work at google.

Software
  • Spin an efficient verification system for distributed software systems (a logic model checker).
  • Feaver a model extraction system for ANSI-C source code: the first step towards the development of a general purpose tool for the verification of distributed systems applications directly from program source text. the system was used at Bell Labs between 1998 and 2000 to exhaustively verify the call-processing software of Lucent's PathStar access server. The source code is available, see the Modex distribution page.
  • Uno A simple static analysis tool for ANSI C programs, based on Ctree 0.14.
  • Ubet a requirements capture and analysis toolset from around 1995, originally called msc/poga, later productized and distributed within Lucent as the uBET tool.
  • Sdlvalid, an early verifier for SDL. the tool was written in 1987/1988, and was used internally for about five years. it was never approved for public release.
  • microtrace a demo awk-script for FSM verification (written 1987).
  • Pico/Popi digital darkroom software (written 1984). For the curious, here is also a tar archive pico.tar with the pre-ansi c source code that includes the little on-the-fly compiler that Ken Thompson and Rob Pike wrote. The compiler in gen.c (also written in 1984) generated machine code for a VAX. Of course, this code will not compile or run on any modern machine. See also Pico's website.

Books

Papers etc.

Little Movies
  • pixelface, 1988, a five minute demo of Pico/Popi (Mpeg 40Mb).
    A portion of the video was shown on CNN Science & Technology report in 1989: see clip.
  • walkman, 1984, a 40 second try to make a little movie, with Rob Pike, Don Mitchell, and Lillian Schwartz (Mpeg 7 Mb).
    A frame from the movie was used for the cover of IEEE Spectrum, June 1984.

Covers, Logos etc.

Photos
  • Portraits, a small selection of the portraits I've taken in the last 25 years or so, mostly with a large studio view camera.
  • Masks and Statues from the collection of Norbert Elias, taken between 1983 and 1987 in Amsterdam
  • Pictures of Tessa, the start of a well-documented life...

Press

Other
http://eis.jpl.nasa.gov/~gh Page last modified March 16, 2006