A Fixpoint Based Encoding for Bounded Model Checking

Alan M. Frisch; Daniel Sheridan; Toby Walsh

doi:10.1007/3-540-36126-X_15

A Fixpoint Based Encoding for Bounded Model Checking

Alan M. Frisch, Daniel Sheridan, Toby Walsh

Computer Science

Research output: Contribution to conference › Paper › peer-review

Abstract

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.

Original language	Undefined/Unknown
Pages	238-255
Number of pages	17
DOIs	https://doi.org/10.1007/3-540-36126-X_15
Publication status	Published - 2002

Access to Document

10.1007/3-540-36126-X_15

http://link.springer.de/link/service/series/0558/bibs/2517/25170238.htm

Cite this

@conference{afaa876012ea48fa8a035a528ca53f6b,

title = "A Fixpoint Based Encoding for Bounded Model Checking",

abstract = "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. ",

author = "Frisch, {Alan M.} and Daniel Sheridan and Toby Walsh",

year = "2002",

doi = "10.1007/3-540-36126-X_15",

language = "Undefined/Unknown",

pages = "238--255",

}

TY - CONF

T1 - A Fixpoint Based Encoding for Bounded Model Checking

AU - Frisch, Alan M.

AU - Sheridan, Daniel

AU - Walsh, Toby

PY - 2002

Y1 - 2002

N2 - 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.

AB - 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.

U2 - 10.1007/3-540-36126-X_15

DO - 10.1007/3-540-36126-X_15

M3 - Paper

SP - 238

EP - 255

ER -