gerard j. holzmann

gerard holzmann

nimble research
cv (short) cv (long)

focus

 software safety, software analysis, formal verification, metrics, logic model checking, distributed systems, multi-threaded software, static analysis, swarm testing, code review methods, requirements capture and analysis, algorithms, user interface design, graphic design, text processing, image processing, technology transfer.

history

 before joining nimble research and jpl/caltech 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. most have found a safe haven elsewhere.

software tools
  • cobra a generic, fast and light-weight, static and dynamic analyzer.
  • 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]
  • GitHub/ncsl 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.
  • GitHub/gh_cpp 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 also 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

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 format, 7 mb).
    a frame from the movie was used for the cover of ieee spectrum, june 1984.

logos

conference posters

  • 3rd nasa formal methods symposium, pasadena, ca, april 2011
  • 18th spin workshop, cliff lodge, snow bird, utah, july 2011
  • 2nd int. conf. on runtime verification, san francisco, ca, september 2011

cds

covers

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. updated april 2014.

press

other
page last modified 7 February 2021