Improving Encoding Efficiency for Bounded Model Checking
Bounded Model Checking (BMC) has played an important role in verification of software, embedded systems and protocols. The idea of BMC is to encode Finite State Machine (FSM) and Linear Temporal Logic (LTL) verification specification into satisfiability (SAT) instances, and then to search for a counterexample via various SA T tools. Improving encoding technology of BMC can generate a SAT instance easy to solve, and therefore is essential to improve the efficiency of BMC. In this paper, we improve the encoding of BMC by combining the characteristic of FSM state transition and semantics of LTL, get a simple and efficient recursion formula which is useful to efficiently generate SAT instances. We present an efficient algorithm to encode the modal operator (safety formula) in BMC. The experiments for comparative analysis shows that this encoding algorithm is more powerful than the existing two mainstream encoding algorithms in both the scale of generated SAT instances and the solving efficiency. The methodology presented in this paper is also valuable for optimization of other modal operator encodings in BMC.
Jinji Yang Kaile Su Qingliang Chen
School of Computer, South China Normal University, Guangzhou, China Dept.of Computer Science, Sun Ya Key laboratory of High Confidence Software Technologies (Peking University), Ministry of Education, Dept.of Computer Science, Jinan university, Guangzhou, China
国际会议
南京
英文
31-38
2008-06-17（万方平台首次上网日期，不代表论文的发表时间）