System complexity grows exponentially as system size and concurrency grow. This makes verification more challenging and put huge pressure on verification team to ensure system correctness without delaying time-to-market. Model checking offers an effective alternative to the traditional simulation-based verification and promises formal proof of system correctness. However, it suffers an unfortunate drawback, state explosion, which limits model checking to small designs. In this talk, compositional methods for scalable model checking will be presented, and we will show how these methods mitigate the state explosion problem thus enabling larger designs and systems to be model checked.
Hao Zheng received his Ph.D. from the ECE department of the University of Utah in 2001. He then worked for IBM as a research scientist for 3 years with major responsibility to extend model checking to the standard VLSI design flow. Since 2004, he has been with the faculty of the CSE department of the USF with the major research focuses on methods and algorithms for scalable concurrent system verification and validation. His other interests include applications of distributed/parallel computing and machine learning to design automation. He received a NSF CAREER Award in 2006, and a USF Outstanding Research Achievement Award in 2007.