The Community for Technology Leaders
RSS Icon
Subscribe
Issue No.06 - June (2004 vol.30)
pp: 403-417
Farn Wang , IEEE Computer Society
ABSTRACT
<p><b>Abstract</b>—Dynamic data-structures with pointer links, which are heavily used in real-world software, cause extremely difficult verification problems. Currently, there is no practical framework for the efficient verification of such software systems. We investigated symmetry reduction techniques for the verification of software systems with C-like indirect reference chains like <tt>x->y->z->w</tt>. We formally defined the model of software with pointer data structures and developed symbolic algorithms to manipulate conditions and assignments with indirect reference chains using BDD technology. We relied on two techniques, inactive variable elimination and process-symmetry reduction in the data-structure configuration, to reduce time and memory complexity. We used binary permutation for efficiency, but we also identified the possibility of an anomaly of false image reachability. We implemented the techniques in tool <b>Red</b> 5.0 and compared performance with Mur<i>ø</i> and SMC against several benchmarks.</p>
INDEX TERMS
Symbolic model checking, pointers, data structure, address manipulation, symmetry reduction, experiments.
CITATION
Farn Wang, Karsten Schmidt, Fang Yu, Geng-Dian Huang, Bow-Yaw Wang, "BDD-Based Safety-Analysis of Concurrent Software with Pointer Data Structures Using Graph Automorphism Symmetry Reduction", IEEE Transactions on Software Engineering, vol.30, no. 6, pp. 403-417, June 2004, doi:10.1109/TSE.2004.15
16 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool