{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T15:21:27Z","timestamp":1725895287145},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642104510"},{"type":"electronic","value":"9783642104527"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-10452-7_1","type":"book-chapter","created":{"date-parts":[[2009,11,4]],"date-time":"2009-11-04T03:37:26Z","timestamp":1257305846000},"page":"1-16","source":"Crossref","is-referenced-by-count":1,"title":["Speeding Up Simulation of SystemC Using Model Checking"],"prefix":"10.1007","author":[{"given":"Nicolas","family":"Blanc","sequence":"first","affiliation":[]},{"given":"Daniel","family":"Kroening","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"1_CR1","first-page":"356","volume-title":"Proceedings of ICCAD 2008","author":"N. Blanc","year":"2008","unstructured":"Blanc, N., Kroening, D.: Race analysis for SystemC using model checking. In: Proceedings of ICCAD 2008, pp. 356\u2013363. IEEE, Los Alamitos (2008)"},{"key":"1_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"467","DOI":"10.1007\/978-3-540-78800-3_36","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"N. Blanc","year":"2008","unstructured":"Blanc, N., Kroening, D., Sharygina, N.: Scoot: A tool for the analysis of SystemC models. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 467\u2013470. Springer, Heidelberg (2008)"},{"key":"1_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"570","DOI":"10.1007\/978-3-540-31980-1_40","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E. Clarke","year":"2005","unstructured":"Clarke, E., Kroening, D., Sharygina, N., Yorav, K.: SATABS: SAT-based predicate abstraction for ANSI-C. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 570\u2013574. Springer, Heidelberg (2005)"},{"key":"1_CR4","doi-asserted-by":"publisher","first-page":"74","DOI":"10.1145\/130616.130623","volume":"1","author":"R.H.B. Netzer","year":"1992","unstructured":"Netzer, R.H.B., Miller, B.P.: What are race conditions? Some issues and formalizations. ACM Lett. Program. Lang. Syst.\u00a01, 74\u201388 (1992)","journal-title":"ACM Lett. Program. Lang. Syst."},{"key":"1_CR5","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1145\/349299.349328","volume-title":"Programming language design and implementation (PLDI)","author":"C. Flanagan","year":"2000","unstructured":"Flanagan, C., Freund, S.N.: Type-based race detection for Java. In: Programming language design and implementation (PLDI), pp. 219\u2013232. ACM, New York (2000)"},{"key":"1_CR6","doi-asserted-by":"publisher","first-page":"391","DOI":"10.1145\/265924.265927","volume":"15","author":"S. Savage","year":"1997","unstructured":"Savage, S., Burrows, M., Nelson, G., Sobalvarro, P., Anderson, T.: Eraser: A dynamic data race detector for multithreaded programs. ACM Trans. Comput. Syst.\u00a015, 391\u2013411 (1997)","journal-title":"ACM Trans. Comput. Syst."},{"key":"1_CR7","first-page":"237","volume-title":"Operating systems principles (SOSP)","author":"D. Engler","year":"2003","unstructured":"Engler, D., Ashcraft, K.: RacerX: Effective, static detection of race conditions and deadlocks. In: Operating systems principles (SOSP), pp. 237\u2013252. ACM, New York (2003)"},{"key":"1_CR8","first-page":"308","volume-title":"Programming language design and implementation (PLDI)","author":"M. Naik","year":"2006","unstructured":"Naik, M., Aiken, A., Whaley, J.: Effective static race detection for Java. In: Programming language design and implementation (PLDI), pp. 308\u2013319. ACM, New York (2006)"},{"key":"1_CR9","doi-asserted-by":"publisher","first-page":"1165","DOI":"10.1109\/TCAD.2008.923410","volume":"27","author":"V. D\u2019Silva","year":"2008","unstructured":"D\u2019Silva, V., Kroening, D., Weissenbacher, G.: A survey of automated techniques for formal software verification. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems (TCAD)\u00a027, 1165\u20131178 (2008)","journal-title":"IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems (TCAD)"},{"key":"1_CR10","first-page":"188","volume-title":"Design Automation Conference (DAC)","author":"M.Y. Vardi","year":"2007","unstructured":"Vardi, M.Y.: Formal techniques for SystemC verification. In: Design Automation Conference (DAC), pp. 188\u2013192. ACM, New York (2007)"},{"key":"1_CR11","first-page":"501","volume-title":"Automated software engineering (ASE)","author":"T. Witkowski","year":"2007","unstructured":"Witkowski, T., Blanc, N., Kroening, D., Weissenbacher, G.: Model checking concurrent Linux device drivers. In: Automated software engineering (ASE), pp. 501\u2013504. ACM, New York (2007)"},{"key":"1_CR12","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1145\/996893.996845","volume":"39","author":"S. Qadeer","year":"2004","unstructured":"Qadeer, S., Wu, D.: KISS: keep it simple and sequential. SIGPLAN Not.\u00a039, 14\u201324 (2004)","journal-title":"SIGPLAN Not."},{"key":"1_CR13","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/503272.503274","volume-title":"POPL 2002: Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages","author":"T. Ball","year":"2002","unstructured":"Ball, T., Rajamani, S.K.: The SLAM project: debugging system software via static analysis. In: POPL 2002: Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pp. 1\u20133. ACM, New York (2002)"},{"key":"1_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","volume-title":"Computer Aided Verification","author":"S. Graf","year":"1997","unstructured":"Graf, S., Sa\u00efdi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 72\u201383. Springer, Heidelberg (1997)"},{"key":"1_CR15","unstructured":"Ball, T., Rajamani, S.: Boolean programs: A model and process for software analysis. Technical Report MSR-TR-2000-14, Microsoft Research (2000)"},{"key":"1_CR16","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/s10703-005-1489-x","volume":"26","author":"P. Godefroid","year":"2005","unstructured":"Godefroid, P.: Software model checking: The VeriSoft approach. Form. Methods Syst. Des.\u00a026, 77\u2013101 (2005)","journal-title":"Form. Methods Syst. Des."},{"key":"1_CR17","first-page":"948","volume-title":"Design Automation Conference (DAC)","author":"A. Sen","year":"2008","unstructured":"Sen, A., Ogale, V., Abadir, M.S.: Predictive runtime verification of multi-processor SoCs in SystemC. In: Design Automation Conference (DAC), pp. 948\u2013953. ACM, New York (2008)"},{"key":"1_CR18","first-page":"110","volume-title":"Principles of programming languages (POPL)","author":"C. Flanagan","year":"2005","unstructured":"Flanagan, C., Godefroid, P.: Dynamic partial-order reduction for model checking software. In: Principles of programming languages (POPL), pp. 110\u2013121. ACM, New York (2005)"},{"key":"1_CR19","doi-asserted-by":"publisher","first-page":"558","DOI":"10.1145\/359545.359563","volume":"21","author":"L. Lamport","year":"1978","unstructured":"Lamport, L.: Time, clocks, and the ordering of events in a distributed system. Commun. ACM\u00a021, 558\u2013565 (1978)","journal-title":"Commun. ACM"},{"key":"1_CR20","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1109\/FMCAD.2006.10","volume-title":"Formal Methods in Computer Aided Design (FMCAD)","author":"C. Helmstetter","year":"2006","unstructured":"Helmstetter, C., Maraninchi, F., Maillet-Contoz, L., Moy, M.: Automatic generation of schedulings for improving the test coverage of systems-on-a-chip. In: Formal Methods in Computer Aided Design (FMCAD), pp. 171\u2013178. IEEE Computer Society, Los Alamitos (2006)"},{"key":"1_CR21","first-page":"936","volume-title":"Design Automation Conference (DAC)","author":"S. Kundu","year":"2008","unstructured":"Kundu, S., Ganai, M., Gupta, R.: Partial order reduction for scalable testing of SystemC TLM designs. In: Design Automation Conference (DAC), pp. 936\u2013941. ACM, New York (2008)"},{"key":"1_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"382","DOI":"10.1007\/978-3-540-78800-3_29","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"C. Wang","year":"2008","unstructured":"Wang, C., Yang, Z., Kahlon, V., Gupta, A.: Peephole partial order reduction. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 382\u2013396. Springer, Heidelberg (2008)"},{"key":"1_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"409","DOI":"10.1007\/3-540-56922-7_34","volume-title":"Computer Aided Verification","author":"D. Peled","year":"1993","unstructured":"Peled, D.: All from one, one for all: On model checking using representatives. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol.\u00a0697, pp. 409\u2013423. Springer, Heidelberg (1993)"},{"key":"1_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"377","DOI":"10.1007\/3-540-58179-0_69","volume-title":"Computer Aided Verification","author":"D. Peled","year":"1994","unstructured":"Peled, D.: Combining partial order reductions with on-the-fly model-checking. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol.\u00a0818, pp. 377\u2013390. Springer, Heidelberg (1994)"},{"key":"1_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-60761-7","volume-title":"Partial-Order Methods for the Verification of Concurrent Systems","author":"P. Godefroid","year":"1996","unstructured":"Godefroid, P.: Partial-Order Methods for the Verification of Concurrent Systems. LNCS. Springer, Heidelberg (1996)"},{"key":"1_CR26","first-page":"521","volume-title":"22nd IEEE International Conference on Automated Software Engineering (ASE)","author":"N. Blanc","year":"2007","unstructured":"Blanc, N., Groce, A., Kroening, D.: Verifying C++ with STL containers via predicate abstraction. In: 22nd IEEE International Conference on Automated Software Engineering (ASE), pp. 521\u2013524. IEEE, Los Alamitos (2007)"},{"key":"1_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1007\/11817963_37","volume-title":"Computer Aided Verification","author":"B. Cook","year":"2006","unstructured":"Cook, B., Podelski, A., Rybalchenko, A.: Terminator: Beyond safety. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 415\u2013418. Springer, Heidelberg (2006)"},{"key":"1_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/10722167_15","volume-title":"Computer Aided Verification","author":"E.M. Clarke","year":"2000","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 154\u2013169. Springer, Heidelberg (2000)"},{"key":"1_CR29","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/s10703-006-0020-3","volume":"30","author":"E. Clarke","year":"2007","unstructured":"Clarke, E., Jain, H., Kroening, D.: Verification of SpecC using predicate abstraction. Form. Methods Syst. Des.\u00a030, 5\u201328 (2007)","journal-title":"Form. Methods Syst. Des."},{"key":"1_CR30","first-page":"101","volume-title":"Formal Methods and Models for Co-Design (MEMOCODE)","author":"D. Kroening","year":"2005","unstructured":"Kroening, D., Sharygina, N.: Formal verification of SystemC by automatic hardware\/software partitioning. In: Formal Methods and Models for Co-Design (MEMOCODE), pp. 101\u2013110. IEEE Computer Society, Los Alamitos (2005)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods: Foundations and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-10452-7_1.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,30]],"date-time":"2021-04-30T07:31:42Z","timestamp":1619767902000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-10452-7_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642104510","9783642104527"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-10452-7_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}