PragaTI (TI India Technical University), VLSI Society of India, and
IEEE Circuits and Systems Society Bangalore Chapter
jointly announce a seminar on

Topic –Scaling Commercial Model Checking to Larger Systems

Date – 18 July 2007
Time – 11.00 AM – 12.00 Noon
Venue – TR-1, Texas Instruments Bangalore
CV Raman Nagar Bangalore 560093

Speaker – Bob Kurshan, Cadence Design Systems










Abstract – ???

Speaker Biography

Robert Kurshan joined Cadence Design Systems, Inc. as a Fellow, in
2001. He manages the Incisive Formal Engines Team, working closely
with Cadence Berkeley Labs and multiple product groups. His work
contributed greatly to Incisive Formal Verifier winning the
Innovation of the Year award at Cadence in 2005. Prior to Cadence,
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 from the University of
Washington in mathematics in 1968, 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). 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 80 technical publications, holds 22 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 a
course he gave at U. C. Berkeley.

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 utilized by Cadence for commercial hardware
verification as part of the Incisive Formal product line and for
constraint-solving in its guided-random Incisive simulation.


This seminar is open to everyone. External participants must send a
note to srihari@... confirming their participation a week prior
to the event. They must arrive at TI Bangalore reception area no
later than 10.45 AM in order to be escorted in.