±¨ ¸æ ÈË: ÁõÉÙÓ¢½ÌÊÚ[ÈÕ±¾·¨Õþ´óѧÍÆËã»ú¿Æѧϵ]
»ã±¨¹¦·ò: 2015Äê7Ô 27ÈÕ£¨ÖÜÒ»£©9:30¡«11:00
»ã±¨µØÖ·: У±¾²¿¶«ÇøÍÆËã»ú´óÂ¥901ÊÒ
Ñû Çë ÈË: çÑ»´¿Û ½ÌÊÚ
Abstract£º
In this talk, a new and practical approach known as testing-based formal verification (TBFV) is first introduced and its application to verifying properties of specifications and programs are then discussed. This approach is expected to strike an effective balance between formal verification and testing by utilizing their advantages and avoiding their weaknesses. The underlying principle is to use well selected data to test whether desired properties expressed as logical formula do not hold and the result can help the developer to determine the quality of the artifact. The biggest advantage of TBFV over the testing and formal verification approaches is the great potential of full automation with the effect of approximation to formal proof in most cases.
Biography£º
Shaoying Liu(ÁõÉÙÓ¢) ½ÌÊÚ£¬ÈÕ±¾³ÛÃûÍÆËã»úר¼Ò£¬ÈÕ±¾·¨Õþ´óѧ½ÌÊÚ£¬Ð±¦GGÍÆËã»ú¹¤³ÌÓë¿ÆѧѧԺ¿Í×ù½ÌÊÚ¡£ÔçÄêÔÚÎ÷°²½»Í¨´óѧ»ñµÃѧʿºÍ˶ʿѧ룬ºóÔÚÓ¢¹úÂü³¹Ë¹ÌØ´óѧ»ñµÃ²©Ê¿Ñ§Î»¡£ÏÖΪIEEEÍÆËã»úѧ»á¸´ÔÓÐÔ¼¼ÊõίԱ»á¸±Ö÷ϯ£¬IEEEÍÆËã»úѧ»á¡¢ACM¡¢ÈÕ±¾Èí¼þ¿ÆѧÓë¼¼Êõѧ»á³ÉÔ±¡£¶àÄêÀ´£¬ËûÔÚÍÆËã»ú¿ÆѧµÄºÜ¶àÁìÓò£¬Ô̺¬´ó¾Ö»¯¹¤³Ì²½Öè¡¢Èí¼þ¿ª·¢²½Öèѧ¡¢Èí¼þ²âÊÔ¡¢¿¿µÃס¸´ÔÓµÄÍÆËã»úϵͳºÍÖÇÄÜÈí¼þ¹¤³Ì»·¾³µÈ·½Ãæ×ö³öÁ˳ÁÒª¹±Ïס£ËûÔÚ³ÛÃû¹ú¼ÊÔÓÖ¾¼°»áÒé°ä·¢Ñ§ÊõÂÛÎÄ150¶àƪ£¬³ö°æ×êÑÐרÖø4²¿£¬Ô̺¬ÔÚSpringer³ö°æÁËרÖø¡¶Formal Engineering for Industrial Software Development¡·¡£ËûÊǹú¼Ê´ó»áµÄÖ÷ϯ¡£ÂÅ´ÎÔÚ¹úÄÚ±íµÄ¶àËù´óѧ½²Ñ§,×÷ѧÊõ»ã±¨¡£
