%0 Journal Article
%T Source-oriented Software Model Checking and its Implementation<br>面向源代码的软件模型检测及其实现
%A HE Kai-duo
%A GU Ming
%A SONG Xiao-yuLI Li
%A LI Jiang
%A <br>何恺铎
%A 顾明
%A 宋晓宇
%A 李力
%A 李江
%J 计算机科学
%D 2009
%I 
%X Model checking on software reliability is always considered meaningful.This paper studied theory and metho-dology on source code verification,utilizing predicate abstraction and counterexample-guided abstraction refinement.Detailed verification framework and its implementation of the self-designed Jchecker,a source-oriented software model checker,were also introduced.
%K Software model checking
%K Source verification
%K Predicate abstraction
%K Abstraction refinement<br>软件模型检测
%K 源程序验证
%K 谓词抽象
%K 抽象求精
%U http://www.alljournals.cn/get_abstract_url.aspx?pcid=5B3AB970F71A803DEACDC0559115BFCF0A068CD97DD29835&cid=8240383F08CE46C8B05036380D75B607&jid=64A12D73428C8B8DBFB978D04DFEB3C1&aid=D751531780CB62FAF2950AC9E42F5F66&yid=DE12191FBD62783C&vid=933658645952ED9F&iid=CA4FD0336C81A37A&sid=866F8A6B640835A7&eid=4E6F5C60B72D9B1C&journal_id=1002-137X&journal_name=计算机科学&referenced_num=1&reference_num=26