Sciweavers

FMICS
2006
Springer

SAT-Based Verification of LTL Formulas

13 years 7 months ago
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...
Wenhui Zhang
Added 22 Aug 2010
Updated 22 Aug 2010
Type Conference
Year 2006
Where FMICS
Authors Wenhui Zhang
Comments (0)