The Verification of Flood Barrier Control Algorithms in Rotterdam

-

10 Years After


AN INTERNATIONAL WORKSHOP ON ADVANCES IN MODEL CHECKING

IN HONOUR OF

GERARD J. HOLZMANN

  NOVEMBER 30, 2006 / DECEMBER 01, 2006

UNIVERSITY OF TWENTE, ENSCHEDE, THE NETHERLANDS


The UT Nieuws about Gerard J. Holzmann:



Gerard Holzmann is the founder of the SPIN model checker, the Swiss army knife of the computer world. To produce software without bugs it is necessary to verify it. The most significant method is model checking: the automatic searching for a model matching the given properties. Because software models are exceptionally large, they require ingenious algorithms to make them receptive to automatic searching.

Gerard Holzmann made model checking what it is today: a practical, automatic technique for software analysis called SPIN. The secret of Holzmann's succes is that he, as the designer, is in the middle of the users of SPIN and knows of their needs. He is a partisan of the theory which he further develops and broadens. He is also an engineer who isn't scared of experimenting with new concepts - for which there is no theory yet. This mixture of research and practical technology makes Holzmann an ideal candidate for an honourary doctorate, according to his honourary promotor Ed Brinksma (part-time professor at the EWI faculty and director of the embedded systems institure at the technical university of Eindhoven.)  (©: UT Nieuws, 7 september 2006, jaargang 41, nr. 24)