Sciweavers

Share
CHARME
2005
Springer

An Analysis of SAT-Based Model Checking Techniques in an Industrial Environment

10 years 6 months ago
An Analysis of SAT-Based Model Checking Techniques in an Industrial Environment
Abstract. Model checking is a formal technique for automatically verifying that a finite-state model satisfies a temporal property. In model checking, generally Binary Decision Diagrams (BDDs) are used to efficiently encode the transition relation of the finite-state model. Recently model checking algorithms based on Boolean satisfiability (SAT) procedures have been developed to complement the traditional BDD-based model checking. These algorithms can be broadly classified into three categories: (1) bounded model checking which is useful for finding failures (2) hybrid algorithms that combine SAT and BDD based methods for unbounded model checking, and (3) purely SAT-based unbounded model checking algorithms. The goal of this paper is to provide a uniform and comprehensive basis for evaluating these algorithms. The paper describes eight bounded and unbounded techniques, and analyzes the performance of these algorithms on a large and diverse set of hardware benchmarks.
Nina Amla, Xiaoqun Du, Andreas Kuehlmann, Robert P
Added 26 Jun 2010
Updated 26 Jun 2010
Type Conference
Year 2005
Where CHARME
Authors Nina Amla, Xiaoqun Du, Andreas Kuehlmann, Robert P. Kurshan, Kenneth L. McMillan
Comments (0)
books