%0 Journal Article
%T Verification of C Programs Using Assume-Guarantee Reuse of Searching<br>基于Assume-Guarantee搜索复用的C程序验证方法
%A YI Xiao-Dong
%A WANG Ji
%A YANG Xue-Jun
%A <br>易晓东
%A 王戟
%A 杨学军
%J 软件学报
%D 2007
%I 
%X This paper presents a novel method,namely Assume-Guarantee reuse of searching,to verify C programs with respect to temporal safety properties.Its idea is to introduce a conservative assume condition for each program location,and to assume that every path starting from the program location will never violate the property if the evaluation of its variables at that location satisfy the assume condition.All the possible execution paths are traversed based on the assume conditions,and the temporal safety property is checked on the fly.If some assume condition is too weak,it will be continually strengthened based on the spurious counterexamples.The presented verification method can try to adopt the weak assume conditions so as to let more execution paths satisfy the conditions and to reuse the searching efforts.Therefore,a significant reduction of verification cost can be achieved.The verification method has been used to verify the initial handshake process of SSL protocol based on the C source code of openssl-0.9.6c.The experimental results demonstrate that the method is both effective and practical.
%K Assume-Guarantee reuse of searching
%K variable abstraction
%K approximated program semantics
%K partial strongest post-condition<br>Assume-Guarantee搜索重用
%K 变量抽象
%K 程序近似语义
%K 部分最强后置条件
%U http://www.alljournals.cn/get_abstract_url.aspx?pcid=5B3AB970F71A803DEACDC0559115BFCF0A068CD97DD29835&cid=8240383F08CE46C8B05036380D75B607&jid=7735F413D429542E610B3D6AC0D5EC59&aid=1DA2F1958CEFAC98&yid=A732AF04DDA03BB3&vid=13553B2D12F347E8&iid=9CF7A0430CBB2DFD&sid=E8101C99E403BAC0&eid=EED5C98ED814B809&journal_id=1000-9825&journal_name=软件学报&referenced_num=0&reference_num=29