By the same authors

A Fixpoint Based Encoding for Bounded Model Checking

Research output: Contribution to conferencePaper



Publication details

DatePublished - 2002
Number of pages17
Original languageUndefined/Unknown


The Bounded Model Checking approach to the LTL model checking problem, based on an encoding to Boolean satisfiability, has seen a growth in popularity due to recent improvements in SAT technology. The currently available encodings have certain shortcomings, particularly in the size of the clause forms that it generates. We address this by making use of the established correspondence between temporal logic expressions and the fixpoints of predicate transformers as used in symbolic model checking. We demonstrate how an encoding based on fixpoints can result in improved performance in the SAT checker.

Discover related content

Find related publications, people, projects, datasets and more using interactive charts.

View graph of relations