Verification of C Programs Using Assume-Guarantee Reuse of Searching
基于Assume-Guarantee搜索复用的C程序验证方法

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.