BMC via dynamic atomicity analysis
Toni Jussila · 2004
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.