loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Fourth International Conference on Application of Concurrency to System Design (ACSD'04)
BMC via Dynamic Atomicity Analysis
Hamilton, Ontario, Canada
June 16-June 18
ISBN: 0-7695-2077-4
ASCII Text
x 
 
Toni Jussila, "BMC via Dynamic Atomicity Analysis," Application of Concurrency to System Design, International Conference on, pp. 197, Fourth International Conference on Application of Concurrency to System Design (ACSD'04), 2004.
 
 
BibTex
x
 
@article{ 10.1109/CSD.2004.1309132,
author = {Toni Jussila},
title = {BMC via Dynamic Atomicity Analysis},
journal ={Application of Concurrency to System Design, International Conference on},
volume = {0},
year = {2004},
isbn = {0-7695-2077-4},
pages = {197},
doi = {http://doi.ieeecomputersociety.org/10.1109/CSD.2004.1309132},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - CONF
JO - Application of Concurrency to System Design, International Conference on
TI - BMC via Dynamic Atomicity Analysis
SN - 0-7695-2077-4
SP
EP
A1 - Toni Jussila,
PY - 2004
KW - null
VL - 0
JA - Application of Concurrency to System Design, International Conference on
ER -
 
Toni Jussila, Helsinki University of Technology, Finland
This paper presents a non-standard execution model and its propositional 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.
Citation:
Toni Jussila, "BMC via Dynamic Atomicity Analysis," acsd, pp.197, Fourth International Conference on Application of Concurrency to System Design (ACSD'04), 2004
Usage of this product signifies your acceptance of the Terms of Use.