Title: Prove Theorems, Find Bugs and Make Profits
Time: Nov. 5, 2:30 PM
Place: 5407 Software Building
Abstract:
Proving correctness of computer programs has long been a pursuit of computer scientists. As computer software and hardware are increasingly used in mission critical projects, functional bugs can have severe consequences.
Research in automated verification is therefore of both theoretical and practical interests. While complete correctness proofs remain elusive, great progress has been made in algorithms that can find critical bugs in large scale programs. In this talk, two bug finding technologies, bounded model checking and assertion synthesis, will be presented. Instead of detailed technical discussions, we will present an overview and focus on the ideas and intuitions behind the development of the technologies. We will also discuss how commercial software tools have been successfully developed based on these technologies and used to verify some of the world’s most complex designs.
Bio:
Dr. Yunshan Zhu is VP of New Technologies at Atrenta. Prior to Atrenta, Dr.
Zhu co-founded NextOp Software Inc. He was the CEO of NextOp until its successful acquisition by Atrenta. At NextOp, Dr. Zhu co-invented the assertion synthesis technology, which is in production use at many leading semiconductor and system companies. Dr. Zhu worked as a researcher in formal verification at Synopsys Advanced Technology Group. Dr. Zhu was also visiting scientist and a post-doc at Carnegie Mellon University where he co-invented the bounded model checking algorithm. Dr. Zhu did his undergraduate study at University of Science and Technology of China and received his Ph.D. in Computer Science from University of North Carolina at Chapel Hill.