|
|
| |
software tools
|
- 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
|
-
the spin model checker - primer and reference manual.
describes the current version of spin, 608 pgs.
addison-wesley publ., isbn 0-321-22862-6, september 2003.
-
design and validation of computer protocols, prentice hall, 1991.
the spin model checker was originally written for inclusion in this book in 1989.
the book contains the full source text (about 5,000 lines) for the original version of spin.
-
the early history of data networks, ieee computer society press
(now wiley publ), 1995.
-
beyond photography -- the digital darkroom, prentice hall, 1988.
first book to coin the term digital darkroom;
it predicted that the days of conventional photograph would be numbered,
which has now come to fruition, though it took a little longer than we thought at the time.
the book, with some background information, is accessible online via the link above.
|
|
|
|
| |
papers
|
- publications, with pdf for most papers
- abstracts for selected 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
|
- the original inferno logo 1996
- cs research center logo (bell labs center 1127) 1997
- spin logo 2000
- nasa/jpl lars center logo 2004
- nfm2011 conference logo 2011
|
|
|
|
| |
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
|
- cd, chess endgames, vols 1-4, (issued by ken thompson, 1991)
(chess-piece and a small part of leonardo da vinci's creation.)
- cd, plan-9 from bell labs, 1st edition, 1992.
(three actors from plan-9, the movie by ed wood)
- cds and cover for floppy disks, plan-9, 2nd edition, 1995
|
|
|
|
| |
covers
|
- at&t technical journal, march/april 1987,
vol 66, issue 2.
(cover with a transformed pico/popi image of peter weinberger's portrait.)
- at&t bell laboratories technical journal, october 1984,
vol 63, no. 8, part 2.
special issue on unix (cover with computer generated graphics.)
- manual covers (2 volumes), plan-9, 2nd edition,
pub. harcourt brace & company, orlando, fl., 1995.
(illustrations from louis figuier, les merveilles de la science, paris 1867)
|
|
|
|
| |
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.
- pictures of tessa,
the start of a well-documented life...
|
|
| |
press
|
-
ICT 2013 Vol. 18, 2013 (in Dutch).
-
interview for The Setup...
-
Gigaom,
code review and analysis process followed for the Mars Science Laboratory
Mission, 2012
-
Caltech Engenious, interview on Safety Critical Software, 2011
-
nasa tech briefs, who's who at nasa, 1 september 2009,
interview with bruce bennett.
-
software development times, 1 may 2009,
interview with jeff feinman.
-
cacm, july 2008,
in search of dependable design, vol. 51, no. 7, pp. 14-16.
a couple of quotes from an interview with leah hoffman.
-
story in ieee computer, jan. 2004
-
interview with ftp online, oct. 2003
-
interview with objectmonkey.com, oct. 2003
-
MIT technology review, february 2003,
brief mention in the category of
software assurance, in article on ``10 emerging technologies that will change the world.''
-
interview with software development magazine (SD magazine), on software verification, september 2002, p.15.
-
NJN new nersey network news,
an interview on software quality aired in the science and technology
segment on march 6, 2002.
-
two dutch journals,
technisch weekblad, no. 17,
and embedded systems, published
interviews (in dutch).
-
infoworld, october 26, 2001
short feature on code debugging.
-
CIO magazine,
august 1, 2001.
brief mention of software verification project.
-
new scientist, 18 november, 2000
-
future of software
column published in FTP magazine in 2000, fawcette publ.
-
a series of columns on smart machines, published in
Inc. technology
|
|
| |
other
|
- ieee harlan d. mills award, may 2015
- nasa
exceptional engineering achievement medal,
october 2012
- acm fellow, june 2012
- caltech cs, faculty associate, may 2007
- jpl fellow, may 2007
- honorary doctorate,
twente university, the netherlands, december 2006
-
acm kanellakis theory and practice award,
may 2006 (with vardi, wolper, and kurshan),
pdf
- us national academy of engineering, elected member 2005.
cs peer committee 2008-2011
-
thomas alva edison patent award (with ken thompson and phil winterbottom),
july 2003
- acm sigsoft
outstanding research award, 2002
-
acm system software award, 2001
(press release march 2002)
|
|