| |
Dr. Kurshan '65 speaks at Meliora Weekend 2002
| Prev | Next | articles |
Posted by gage@math.rochester.edu, 10/9/02 at 3:18:07 PM.
For Meliora weekend the math department is again having an alumnus come speak. Dr. Robert Kurshan, class of '65, did his graduate work in mathematics at the University of Washington. He has spent much of his career at Bell Labs Research (now Lucent) working on both "pure math" problems and applications of mathematics to problems in technology.
One of his long time interests is in program verification. How can you be sure that a computer program will perform correctly under unexpected circumstances? Once a program reaches a certain level of complexity it can't be checked simply by exhaustive testing -- strategy is required and, if possible, automation. Sometimes pure math is the best way to understand a very practical problem!
The necessity of the best possible error checking is emphasized by the millions of dollars lost in high profile space probe disasters caused by the unexpected behaviors of programs controlling the rockets.
This lecture is designed for the general public and everyone is encouraged to attend. An open house at 4pm in the Undergraduate Math Lounge (9th floor of Hylan) precedes the lecture.
Talk Info
Program Verification
Dr. Robert P. Kurshan, '65
Fellow, Cadence Design Systems
5:00 pm, Friday, October 11 -- 209 CSB (Computer Science Building)
Reception and open house: 4:00 pm, Friday, October 11 --
Undergraduate Math Lounge, 9th floor Hylan
ABSTRACT: I will discuss a method for checking the correctness of certain types of computer programs. The method is based on a mathematical analysis of the program. This is in contrast with customary testing based upon program execution. The new form of analysis has been found to be more reliable than conventional testing, and is being used commercially in the development of programs implemented as integrated circuits. The same methodology is applicable to the development of ``control-intensive'' software programs as well. An interesting part of the story is the technology transfer process: how did an idea get from research to a commercially successful product. I will spend a few minutes on this as well.
More background
For more background here is a link to a press release and the article Program Verification which Dr. Kurshan wrote for the AMS Notices in May 2000.
Brief Bio:
Robert Kurshan is a fellow at Cadence Design Systems. Before that he was a Distinguished Member of Technical Staff at Bell Laboratories, Murray Hill, NJ. He has worked there since receiving his Ph.D in mathematics in 1968, from the University of Washington. He spent two years as Visiting Professor at the Technion (Haifa, Israel) in the departments of Mathematics and Electrical Engineering. 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 60 technical publications, holds eight 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. 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 which is developed in this book. COSPAN has been in use (and continuous development) since 1986, having been applied to a number of commercial projects, as well as having been licensed to numerous universities for educational use. Currently, COSPAN is marketed for commercial use by Cadence Design Systems, Inc., under the trademark FormalCheck.
| Prev | Next | articles |