SAT-Based Verification of LTL Formulas

Abstract. Bounded model checking (BMC) based on satisfiability testing (SAT) has been introduced as a complementary technique to BDDbased symbolic model checking of LTL properties in recent years and a lot of successful work has been done with this approach. The basic idea is to search for a counter example of a particular length and to generate a propositional formula that is satisfied iff such a counter example exists. An over approximation of the length that need to be checked in order to certify that the system is error free is usually too big, such that it is not practical to use this approach for checking systems that are error free with respect to given properties. Even if we know the exact threshold, for a reasonably large system, this threshold would possibly also be large enough to make the verification become intractable due to the complexity of solving the corresponding SAT instance. This study is on a different direction and the aim of this study is verification of valid p...

• Type: Conference
• Year: 2006
• Where: FMICS
• Authors: Wenhui Zhang
• Keywords: Counter Example, FMICS 2006, Formal Methods, LTL Properties, Model Checking