Paper Info
Title
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.
Year
DOI
Venue
2005
10.1007/11560548_20
CHARME
Keywords
Field
DocType
unbounded technique,unbounded model checking,boolean satisfiability,model checking,unbounded model checking algorithm,comprehensive basis,bounded model checking,binary decision diagrams,finite-state model,sat-based model checking technique,traditional bdd-based model checking,industrial environment,satisfiability,decision diagram,hybrid algorithm
Abstraction model checking,Discrete mathematics,Model checking,Computer science,Boolean satisfiability problem,Algorithm,Binary decision diagram,Formal specification,Theoretical computer science,Finite-state machine,Boolean algebra,Formal methods
Conference
Volume
ISSN
ISBN
3725
0302-9743
3-540-29105-9
Citations 
PageRank 
References 
53
2.36
25
Authors
5
Name
Order
Citations
PageRank
Nina Amla131816.23
Xiaoqun Du222512.32
Andreas Kuehlmann31217105.62
Robert P. Kurshan4674125.85
Kenneth L. McMillan53332269.05