2006 | OriginalPaper | Buchkapitel
Improved SAT Based Bounded Model Checking
verfasst von : Conghua Zhou, Decheng Ding
Erschienen in: Theory and Applications of Models of Computation
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
The usefulness of Bounded Model Checking(BMC) based on propositional satisfiability methods has recently proven its efficacy for bug hunting. The basic idea is to search for a counterexample in executions whose length is bounded by some integer
k
. In fact, for some properties some bounded paths are equivalent. In the original Bounded Model Checking equivalent bounded paths may be searched repeatedly. Therefore some searches are redundant. In this paper with respect to some properties we exploit new encoding for Bounded Model Checking such that we can avoid searching for redundant bounded paths.