{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,1]],"date-time":"2025-11-01T02:31:10Z","timestamp":1761964270853,"version":"3.41.0"},"reference-count":40,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2010,5,1]],"date-time":"2010-05-01T00:00:00Z","timestamp":1272672000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100004963","name":"Seventh Framework Programme","doi-asserted-by":"publisher","award":["ICT-216679"],"award-info":[{"award-number":["ICT-216679"]}],"id":[{"id":"10.13039\/501100004963","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000028","name":"Semiconductor Research Corporation","doi-asserted-by":"publisher","award":["2006-TJ-1539"],"award-info":[{"award-number":["2006-TJ-1539"]}],"id":[{"id":"10.13039\/100000028","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/G026254\/1"],"award-info":[{"award-number":["EP\/G026254\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100003006","name":"Eidgen\u00f6ssische Technische Hochschule Z\u00fcrich","doi-asserted-by":"publisher","award":["TH-21\/05-1"],"award-info":[{"award-number":["TH-21\/05-1"]}],"id":[{"id":"10.13039\/501100003006","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Des. Autom. Electron. Syst."],"published-print":{"date-parts":[[2010,5]]},"abstract":"<jats:p>SystemC is a system-level modeling language that offers a wide range of features to describe concurrent systems at different levels of abstraction. The SystemC standard permits simulators to implement a deterministic scheduling policy, which often hides concurrency-related design flaws. We present a novel compiler for SystemC that integrates a very precise formal race analysis by means of model checking. Our compiler produces a simulator that uses the outcome of the analysis to perform partial order reduction. The key insight to make the model checking engine scale is to apply it only to tiny fractions of the SystemC model. We show that the outcome of the analysis is not only valuable to eliminate redundant context switches at runtime, but can also be used to diagnose race conditions statically. In particular, our analysis is able to reveal races that can remain undetected during simulation and is able to formally prove the absence of races.<\/jats:p>","DOI":"10.1145\/1754405.1754406","type":"journal-article","created":{"date-parts":[[2010,6,8]],"date-time":"2010-06-08T12:37:24Z","timestamp":1276000644000},"page":"1-32","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":33,"title":["Race analysis for systemc using model checking"],"prefix":"10.1145","volume":"15","author":[{"given":"Nicolas","family":"Blanc","sequence":"first","affiliation":[{"name":"ETH Zurich, Zurich, Switzerland"}]},{"given":"Daniel","family":"Kroening","sequence":"additional","affiliation":[{"name":"Oxford University, Welington Square, UK"}]}],"member":"320","published-online":{"date-parts":[[2010,6,10]]},"reference":[{"key":"e_1_2_1_1_1","unstructured":"Ball T. and Rajamani S. 2000. Boolean programs: A model and process for software analysis. Tech. rep. MSR-TR-2000-14 Microsoft Research.  Ball T. and Rajamani S. 2000. Boolean programs: A model and process for software analysis. Tech. rep. MSR-TR-2000-14 Microsoft Research."},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503274"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/309847.309942"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1321631.1321724"},{"volume-title":"Proceedings of the IEEE International Conference on Computer-Aided Design (ICCAD'08)","author":"Blanc N.","key":"e_1_2_1_5_1","unstructured":"Blanc , N. and Kroening , D . 2008. Race analysis for SystemC using model checking . In Proceedings of the IEEE International Conference on Computer-Aided Design (ICCAD'08) . IEEE, 356--363. Blanc, N. and Kroening, D. 2008. Race analysis for SystemC using model checking. In Proceedings of the IEEE International Conference on Computer-Aided Design (ICCAD'08). IEEE, 356--363."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792781"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-006-0020-3"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31980-1_40"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/775832.775928"},{"volume-title":"Proceedings of the 12th International Conference on Computer Aided Verification (CAV'00)","author":"Clarke E. M.","key":"e_1_2_1_10_1","unstructured":"Clarke , E. M. , Grumberg , O. , Jha , S. , Lu , Y. , and Veith , H . 2000. Counterexample-Guided abstraction refinement . In Proceedings of the 12th International Conference on Computer Aided Verification (CAV'00) . Lecture Notes in Computer Science. Springer, 154--169. Clarke, E. M., Grumberg, O., Jha, S., Lu, Y., and Veith, H. 2000. Counterexample-Guided abstraction refinement. In Proceedings of the 12th International Conference on Computer Aided Verification (CAV'00). Lecture Notes in Computer Science. Springer, 154--169."},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_37"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2008.923410"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/945445.945468"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/349299.349328"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040315"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"e_1_2_1_17_1","series-title":"Lecture Notes in Computer Science","volume-title":"Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem","author":"Godefroid P.","unstructured":"Godefroid , P. 1996. Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem . Lecture Notes in Computer Science . Springer . Godefroid, P. 1996. Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem. Lecture Notes in Computer Science. Springer."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-005-1489-x"},{"volume-title":"Proceedings of the 9th International Conference on Computer Aided Verification (CAV'97)","author":"Graf S.","key":"e_1_2_1_19_1","unstructured":"Graf , S. and Sa\u00efdi , H . 1997. Construction of abstract state graphs with PVS . In Proceedings of the 9th International Conference on Computer Aided Verification (CAV'97) . Lecture Notes in Computer Science. Springer, 72--83. Graf, S. and Sa\u00efdi, H. 1997. Construction of abstract state graphs with PVS. In Proceedings of the 9th International Conference on Computer Aided Verification (CAV'97). Lecture Notes in Computer Science. Springer, 72--83."},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2006.10"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_2_1_22_1","first-page":"1666","article-title":"SystemC language reference manual","author":"Std","year":"2005","unstructured":"IEEE Std . 2005 . SystemC language reference manual . IEEE Standard 1666 - 2005 . IEEE Std. 2005. SystemC language reference manual. IEEE Standard 1666-2005.","journal-title":"IEEE Standard"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/MEMCOD.2005.1487900"},{"volume-title":"Proceedings of the 4th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI'03)","author":"Kroening D.","key":"e_1_2_1_24_1","unstructured":"Kroening , D. and Strichman , O . 2003. Efficient computation of recurrence diameters . In Proceedings of the 4th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI'03) . Springer, 298--309. Kroening, D. and Strichman, O. 2003. Efficient computation of recurrence diameters. In Proceedings of the 4th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI'03). Springer, 298--309."},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1391469.1391706"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/359545.359563"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/1133981.1134018"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/130616.130623"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.5555\/647762.735490"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.5555\/647763.735529"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/996893.996845"},{"volume-title":"Proceedings of the Conference on Design, Automation and Test in Europe (DATE'01)","author":"Ruf J.","key":"e_1_2_1_32_1","unstructured":"Ruf , J. , Hoffmann , D. , Gerlach , J. , Kropf , T. , Rosenstiehl , W. , and Mueller , W . 2001. The simulation semantics of SystemC . In Proceedings of the Conference on Design, Automation and Test in Europe (DATE'01) . IEEE Press, 64--70. Ruf, J., Hoffmann, D., Gerlach, J., Kropf, T., Rosenstiehl, W., and Mueller, W. 2001. The simulation semantics of SystemC. In Proceedings of the Conference on Design, Automation and Test in Europe (DATE'01). IEEE Press, 64--70."},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.5555\/789083.1022755"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/265924.265927"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1109\/MEMCOD.2005.1487903"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/1391469.1391708"},{"key":"e_1_2_1_37_1","unstructured":"Slonneger K. and Kurtz B. 1995. Domain theory and fixed-point semantics. In Formal Syntax and Semantics of Programming Languages: A Laboratory Based Approach. Addison-Wesley Longman Publishing Boston MA 341--394.   Slonneger K. and Kurtz B. 1995. Domain theory and fixed-point semantics. In Formal Syntax and Semantics of Programming Languages: A Laboratory Based Approach. Addison-Wesley Longman Publishing Boston MA 341--394."},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/1278480.1278527"},{"key":"e_1_2_1_39_1","doi-asserted-by":"crossref","unstructured":"Wang C. Yang Z. Kahlon V. and Gupta A. 2008. Peephole partial order reduction. In Proceedings of the Workshop on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Lecture Notes in Computer Science. Springer 382--396.   Wang C. Yang Z. Kahlon V. and Gupta A. 2008. Peephole partial order reduction. In Proceedings of the Workshop on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Lecture Notes in Computer Science. Springer 382--396.","DOI":"10.1007\/978-3-540-78800-3_29"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/1321631.1321719"}],"container-title":["ACM Transactions on Design Automation of Electronic Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1754405.1754406","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1754405.1754406","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T11:22:50Z","timestamp":1750245770000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1754405.1754406"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,5]]},"references-count":40,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2010,5]]}},"alternative-id":["10.1145\/1754405.1754406"],"URL":"https:\/\/doi.org\/10.1145\/1754405.1754406","relation":{},"ISSN":["1084-4309","1557-7309"],"issn-type":[{"type":"print","value":"1084-4309"},{"type":"electronic","value":"1557-7309"}],"subject":[],"published":{"date-parts":[[2010,5]]},"assertion":[{"value":"2009-05-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2010-02-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2010-06-10","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}