Skip to main content

HVC 2009
Haifa Verification Conference 2009

October 19-22, 2009
Organized by IBM R&D Labs in Israel

image: IBM and Haifa

David Harel

Can We Verify an Elephant?

The talk shows the way techniques from computer science and software engineering can be applied beneficially to research in the life sciences. We will discuss the idea of comprehensive and realistic modeling of biological systems, where we try to understand and analyze an entire system in detail, utilizing in the modeling effort all that is known about it. I will address the motivation for such modeling and the philosophy underlying the techniques for carrying it out, as well as the crucial "verification" question of when such models are to be deemed valid, or complete. The examples I will present will be from among the biological modeling efforts my group has been involved in: T cell development in the thymus, lymph node behavior, organogenesis of the pancreas, fate determination in the reproductive system of C. elegans , and a generic cell model. The ultimate long-term "grand challenge" is to produce an interactive, dynamic, computerized model of an entire multi-cellular organism, such as the C. elegans nematode worm, which is complex, but well-defined in terms of anatomy and genetics. The challenge is to construct a full, true-to-all-known-facts, 4-dimensional, fully animated model of the development and behavior of this worm (or of a comparable multi-cellular animal), which is easily extendable as new biological facts are discovered.

Prof. David Harel has been at the Weizmann Institute of Science in Israel since 1980, and is incumbent of the William Sussman Professorial Chair. He was Head of the Department of Applied Mathematics and Computer Science from 1989 to 1995, and was Dean of the Faculty of Mathematics and Computer Science from 1998 for seven years. He currently heads the John von Neumann Minerva Center for the Development of Reactive Systems.

He received a BSc from Bar-Ilan University (1974), an MSc from Tel-Aviv University (1976) and a PhD from the Massachusetts Institute of Technology (1978). He has spent two years at IBM's Yorktown Heights research center, sabbatical years at Carnegie-Mellon University, Cornell University and the University of Edinburgh, and shorter visiting positions at IBM, Lucent Technologies Bell Labs, DEC, NASA, University of Birmingham, Verimag, the National University of Singapore and Microsoft Research Cambridge. From 1991 to 1999 he was an adjunct professor at the Open University of Israel. He was also co-founder of I-Logix, Inc. in 1984, which was acquired by Telelogic in 2006, which, in turn, was acquired by IBM in 2008.

He has devoted part of his time to educational and expository work: In 1984 he delivered a lecture series on Israeli radio (see the book version|), and in 1998 he hosted a series of programs on Israeli television. Some of his writing is intended for a general audience; see, for example, Computers Ltd.: What They Really Can't Do (2000) and Algorithmics: The Spirit of Computing (1987, 1992, 2004).

His awards include the ACM Karlstrom Outstanding Educator Award (1992), the Stevens Award in Software Development Methods (1996), the Israel Prize in Computer Science (2004), t he ACM SIGSOFT Outstanding Research Award (2006), the ACM Software System Award (2007), the ACM SIGSOFT Impact Paper Award (2008), and honorary degrees from the University of Rennes (2005), the Open University of Israel (2006) and the University of Milano-Bicocca(2007). He is a Fellow of the ACM (1994), of the IEEE (1995) and of the AAAS (2007), and was elected member of the Academia Europaea (2006).

Contact Information

Proceedings Publication

Springer Lecture Notes in Computer Science