DocumentCode
3114769
Title
BMC via dynamic atomicity analysis
Author
Jussila, Toni
Author_Institution
Lab. for Theor. Comput. Sci., Helsinki Univ. of Technol., Hut, Finland
fYear
2004
fDate
16-18 June 2004
Firstpage
197
Lastpage
206
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;
fLanguage
English
Publisher
ieee
Conference_Titel
Application of Concurrency to System Design, 2004. ACSD 2004. Proceedings. Fourth International Conference on
Print_ISBN
0-7695-2077-4
Type
conf
DOI
10.1109/CSD.2004.1309132
Filename
1309132
Link To Document