Title :
BMC via dynamic atomicity analysis
Author_Institution :
Lab. for Theor. Comput. Sci., Helsinki Univ. of Technol., Hut, Finland
Abstract :
This work presents a nonstandard execution model and its proportional encoding for effective bounded model checking of reachability properties. The execution model allows several visible actions from a single system component to be merged dynamically to an atomic block. Thus the bound needed to detect a violation of a property can be reduced. An implementation and results from several test cases are provided.
Keywords :
formal verification; reachability analysis; state-space methods; atomic block; bounded model checking; dynamic atomicity analysis; nonstandard execution model; reachability properties; system component; Computer science; Encoding; Hardware; Independent component analysis; Interleaved codes; Laboratories; Logic; Software systems; Testing; Upper bound;
Conference_Titel :
Application of Concurrency to System Design, 2004. ACSD 2004. Proceedings. Fourth International Conference on
Print_ISBN :
0-7695-2077-4
DOI :
10.1109/CSD.2004.1309132
