Formal Verification and Code Clone Detection

发布时间:2014-12-04  阅读次数:2074
 Masahiro Fujita
VLSI Design and Education Center (VDEC), 
University of Tokyo

Biography of Masahiro Fujita
Masahiro Fujita received his Ph.D. in Information Engineering from the University of Tokyo in 1985. From 1993 to 2000, he was director at Fujitsu Laboratories of America. Since March 2000, he has been a professor at VLSI Design and Education Center of the University of Tokyo. He has been involved in a Japanese governmental research project, and has authored and co-authored 10 books, and more than 200 publications. He has been involved as program and steering committee member in many prestigious conferences.

Talk 1: Hardware partial synthesis and automatic corrections of hardware designs. 
In this talk, we formulate the partial logic synthesis and automatic correction of logical bugs as Quantified Boolean Formula (QBF) and solve it as incremental SAT problem. Our method can generate very small numbers of test vectors by which the target designs can be 100% verified. 
Talk 2: Program code clone detection and its application to equivalence checking
In this talk, we present a way to detect code clones through graph matching. Our graph matching first identifies conflicts among nodes of the two which are represented as Conflict Graph (CD). From CD, we extract Maximum Independent Set (IMS) as matching portions of the original programs. By using appropriate definition on conflicts when generating CD, we can deal with varieties of equivalence/non- equivalence on the programs to be compared. We show some results on recognition of similarity/difference for C codes.
地点:会议室          时间:2014年12月9日  10:00-11:00


地址:中国 上海曹安公路4800号同济大学软件学院



 Copyright© 2017 同济大学软件学院

技术支持: 上海维程