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, code review methods, 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 (now retired). one by one, the others all found a safe haven elsewhere.

Software
  • spin efficient verification system for distributed software systems (a logic model checker).
  • swarm pre-processor for spin, to setup swarm verification jobs on large numbers of cpus.
  • scrub -- a peer code review support tool, used for safety- and mission-critical code. not yet available outside nasa.
  • uno simple static analysis tool for ANSI C programs, based on Ctree 0.14. [see also this overview]
  • ncsl.tar.gz line counter for C and C++ that reports the raw nr of lines, nr of non-comment and non-blank lines and the nr of comments.
  • gh_cpp.tar.gz implementation of the C preprocessor, with some additional checking capabilities (can explain macro-expansions, and can check a small subset of the misra-c 2004 rules).
  • older things (and mostly no longer kept up to date):
    • feaver 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.
    • ubet requirements capture and analysis toolset from around 1995, originally called msc/poga, productized and supported within Lucent as the uBET tool, but later abandoned when Lucent more or less broke up.
    • 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 small demo awk-script for FSM verification, written 1987.
    • pico/popi digital darkroom software (written 1984). 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 (both now at google). the compiler in gen.c (from 1984) generated machine code for a VAX. this code will of course 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
Page last modified 8 May 2009