%0 Journal Article
%T Software Model Checking Based on Abstract-verify-refine Paradigm<br>基于抽象-验证-细化范例的软件模型检测
%A LIU Ji-Feng
%A SUN Ji-Gui
%A <br>刘吉锋
%A 孙吉贵
%J 计算机科学
%D 2006
%I 
%X How to assure the correctness and reliability of software systems is one of the main problems in software development. Being an important automatic verification technique, Model checking is more and more successful in software analysis and verification. This paper presents a survey to software model checking based on abstract-verify-reflne paradigm, using SLAM at Microsoft and BLAST at UC Berkeley as examples.
%K Model checking
%K Software model checking
%K Predicate abstraction
%K Counterexample-driven refinement<br>模型检测
%K 软件模型检测
%K 谓词抽象
%K 反例驱动的细化
%U http://www.alljournals.cn/get_abstract_url.aspx?pcid=5B3AB970F71A803DEACDC0559115BFCF0A068CD97DD29835&cid=8240383F08CE46C8B05036380D75B607&jid=64A12D73428C8B8DBFB978D04DFEB3C1&aid=00F2584066C66FC5&yid=37904DC365DD7266&vid=27746BCEEE58E9DC&iid=59906B3B2830C2C5&sid=627456E7977439A4&eid=89AC6B0ADBEA2741&journal_id=1002-137X&journal_name=计算机科学&referenced_num=0&reference_num=29