Paper Info
Title
A new approach to bounded model checking for branching time logics
Abstract
Bounded model checking (BMC) is a technique for overcoming the state explosion problem which has gained wide industrial acceptance. Bounded model checking is typically applied only for linear-time properties, with a few exceptions, which search for a counter-example in the form of a tree-like structure with a pre-determined shape. We suggest a new approach to bounded model checking for universal branching-time logic, in which we encode an arbitrary graph and allow the SAT solver to choose both the states and edges of the graph. This significantly reduces the size of the counter-example produced by BMC. A dynamic completeness criterion is presented which can be used to halt the bounded model checking when it becomes clear that no counterexample can exist. Thus, verification of the checked property can also be achieved. Experiments show that our approach outperforms another recent encoding for µ-calculus on complex ACTL properties.
Year
DOI
Venue
2007
10.1007/978-3-540-75596-8_29
ATVA
Keywords
Field
DocType
state explosion problem,sat solver,bounded model checking,complex actl property,arbitrary graph,time logic,dynamic completeness criterion,new approach,recent encoding,linear-time property,pre-determined shape,linear time
Discrete mathematics,Abstraction model checking,ENCODE,Model checking,Computer science,Boolean satisfiability problem,Algorithm,Theoretical computer science,Counterexample,Completeness (statistics),Encoding (memory),Bounded function
Conference
Volume
ISSN
ISBN
4762
0302-9743
3-540-75595-0
Citations 
PageRank 
References 
4
0.53
13
Authors
2
Name
Order
Citations
PageRank
Rotem Oshman145622.52
Orna Grumberg24361351.99