Reduction Method of Bounded Model Checking Based on SAT Tool
Guoqing Wu · Jisuanji gongcheng · 2010
Bounded model checking is mainly used to detect the property in the path.This paper proposes an encode method which is used to extend the LTL formulas in path,then bounded model checking can be reduced to the problem of whether the propositional logic formula is satisfiable or not,and SAT checking tool can be used to complete the process.The reducing process is proved to be correct and complete.An specific example is given to show the validity of the method.