Knowledge Center ➜ People

Robert Kurshan

Developer of COSPAN


Robert Kurshan is now retired
Until late 2014 he was a distinguished engineer at Cadence and has been there since 2001.

Kurshan was a Distinguished Member of Technical Staff at Bell Laboratories, Murray Hill, NJ. Until 1995 he worked in the Mathematics Research Center and after that in the Computer Science Research Center.

He began work in formal verification in 1983 and designed and built the COSPAN verification system together with Zvi Har’El, Ronald H. Hardin, and a number of others. This work is described in the book Computer-Aided Verification of Coordinating Processes. COSPAN has been in use since 1986, and was commercialized under the trademark FormalCheck. This was the basis for the Cadence formal verification tool until 2005 when it was replaced by Incisive Formal verifier – an integration of COSPAN and SAT-based technology from Cadence Berkeley Labs.

Kurshan received his Ph.D in mathematics in 1968, from the University of Washington in homological algebra.

Books by Kurshan

Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach (Princeton Series in Computer Science)

Verification of Digital and Hybrid Systems (Nato ASI Subseries F:)