Robert Kurshan, Cadence Design Systems
Email: rkurshan@cadence.com.
Tuesday, July 13, 8:30AM
Historically, what have been called "testing" and "model checking" have been considered polar opposites in that testing has been viewed as an ad hoc user-guided process, whereas model checking has been viewed as an algorithmic fully automatic process.
In fact, neither of these views were completely accurate. More interesting is that recently testing and model checking have been moving toward each other, testing becoming more algorithmic and using model checking as a subroutine.
I will talk about this merger in the fitting venue of the first joint meeting of ISSTA and CAV, representing the professional directions of testing and model checking.
Robert Kurshan joined Cadence Design Systems, Inc. as a Fellow, in 2001. Before that, he was a Distinguished Member of Technical Staff at Bell Laboratories, Murray Hill, NJ, until his retirement in 2001. He worked at Bell Labs since receiving his Ph.D in mathematics in 1968, from the University of Washington under James Jans, in homological algebra. Under special arrangement with Bell Labs, he spent two years as Visiting Professor at the Technion (Haifa, Israel) in the departments of Mathematics (1975-76) and Electrical Engineering (1984-85). In addition, he has taught courses at U.C. Berkeley and N.Y.U. At Bell Labs, he did research in periodic sequences, digital filtering and approximation theory, before he began work in formal verification in 1983. He is an author of over 85 technical publications, holds 25 patents in communications, digital filtering and verification, and is the author of the book Computer-Aided Verification of Coordinating Processes (Princeton Univ. Press, 1994) which is based upon courses he gave at U. C. Berkeley and the Technion.
In connection with his work in verification, he designed and built the COSPAN verification system together with Zvi Har'El, Ronald H. Hardin, and a number of others, based upon the theory that is developed in his book. COSPAN has been in use (and continuous development) since 1986, having been applied directly to a number of commercial projects inside AT&T, Lucent, NCR and Intel, as well as having been licensed to numerous universities for educational use. Currently, COSPAN is marketed by Cadence Design Systems, Inc. for commercial hardware verification, under the trademarks FormalCheck and Incisive Static Verifier (ISV). In 1998, FormalCheck won the Innovation of the Year Award, from EDN. More recently, SAT-based algorithms from Cadence Berkeley Labs have been integrated into COSPAN, which has been released in a new simplified tool for fully automated assertion-based verification, ISV. Other related activities include constraint solving for a number of applications ranging from circuit optimization to automatic test bench generation and use of COSPAN to simplify waveforms that lead to design errors.
David Harel, Weizmann Institute of Science
Email: dharel@weizmann.ac.il.
Wednesday, July 14, 1:30PM
The talk will describe the highlights of the play-in/play-out approach to specifying the behavior of reactive systems using the LSCs language. Emphasis will be made on the underlying inter-object philosophy, and on the "smart" play-out mode, whereby execution is guided by the use of model-checking. We thus employ verification techniques to run programs, not only to prove them correct. The entire setup could lead to a new way of programming, accessible to a wider spectrum of people.
David Harel has been a faculty member at the Weizmann Institute of Science in Israel since 1980, and is incumbent of the William Sussman Professorial Chair in Mathematics. He was Head of the Department of Applied Mathematics and Computer Science from 1989 to 1995, and has been Dean of the Faculty of Mathematics and Computer Science since 1998. He is also co-founder of I-Logix, Inc., Andover, MA, and of SenseIT Technologies, Ltd. (DigiScents Israel). Activity in the latter company stopped with the fall of the Nasdaq in April 2001. He received his B.Sc. from Bar-Ilan University in 1974, his M.Sc. from Tel-Aviv University in 1976 and his PhD from the Massachusetts Institute of Technology in 1978. He has spent two years at IBM's Yorktown Heights research center, sabbatical years at Carnegie-Mellon and Cornell Universities, and shorter visiting positions at IBM, Lucent Technologies Bell Labs, DEC, NASA, University of Birmingham, Verimag, and the National University of Singapore. He was also an adjunct professor at the Open University of Israel between 1991 and 1999.
In the past Dr. Harel has worked in several areas of theoretical computer science, including computability theory, especially levels of undecidability, logics of programs, database theory, and automata theory. Over the years his activity in these areas has diminished, and he has become involved in several other areas, including software and systems engineering, object-oriented analysis and design, visual languages, layout of diagrams, modeling and analysis of biological systems, and the synthesis and communication of smell. He has published widely on these topics. He is the inventor of the language of statecharts, and co-inventor of live sequence charts, and was part of the team that designed the tools Statemate (1984-1987), Rhapsody (1997) and the Play-Engine (2003). His work is central to the behavioral aspects of the UML.
Dr. Harel devotes part of his time to expository work: In 1984 he delivered a lecture series on Israeli radio, and in 1998 he hosted a series of programs on Israeli television. Some of his writing is intended for a general audience. He has received a number of awards, including the ACM Karlstrom Outstanding Educator Award (1992), the Israeli Prime Minister's Award for Software (1997), and the Israel Prize in Computer Science (2004). His book, Algorithmics: The Spirit of Computing, was the Spring 1988 Main Selection of the Macmillan Library of Science. He is a Fellow of the ACM and of the IEEE.