Paper Info
Title
Decomposing Image Computation for Symbolic Reachability Analysis Using Control Flow Information
Abstract
The main challenge in BDD-based symbolic reachability analysis is represented by the sizes of the intermediate decision diagrams obtained during image computations. Methods proposed to mitigate this problem fall broadly into two categories: Search strategies that depart from breadth-first search, and efficient techniques for image computation. In this paper we present an algorithm that belongs to the latter category. It exploits define-use information along executable paths extracted from the control-flow graph of the model being analyzed; this information enables an effective constraining of the transition relation and a decomposition of the image computation process that often leads to much smaller intermediate BDDs. Our experiments confirm that this reduction in the size of the representation of state sets translates in significant decreases in CPU and memory requirements.
Year
DOI
Venue
2006
10.1109/ICCAD.2006.320120
San Jose, CA
Keywords
Field
DocType
binary decision diagrams,flow graphs,image processing,reachability analysis,BDD-based symbolic reachability analysis,binary decision diagram,breadth-first search,control flow information,control-flow graph,image computation
Graph,Computer science,Control flow,Image processing,Algorithm,Exploit,Theoretical computer science,Reachability,Computation,Executable
Conference
ISSN
ISBN
Citations 
1092-3152 E-ISBN : 1-59593-389-1
1-59593-389-1
5
PageRank 
References 
Authors
0.50
25
2
Name
Order
Citations
PageRank
David Ward150.50
Fabio Somenzi23394302.47