{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T05:15:45Z","timestamp":1743138945675,"version":"3.40.3"},"publisher-location":"Cham","reference-count":26,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319633893"},{"type":"electronic","value":"9783319633909"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-63390-9_11","type":"book-chapter","created":{"date-parts":[[2017,7,12]],"date-time":"2017-07-12T08:53:50Z","timestamp":1499849630000},"page":"197-216","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Abstract Interpretation with Unfoldings"],"prefix":"10.1007","author":[{"given":"Marcelo","family":"Sousa","sequence":"first","affiliation":[]},{"given":"C\u00e9sar","family":"Rodr\u00edguez","sequence":"additional","affiliation":[]},{"given":"Vijay","family":"D\u2019Silva","sequence":"additional","affiliation":[]},{"given":"Daniel","family":"Kroening","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,7,13]]},"reference":[{"key":"11_CR1","doi-asserted-by":"crossref","unstructured":"Abdulla, P., Aronis, S., Jonsson, B., Sagonas, K.: Optimal dynamic partial order reduction. In: Principles of Programming Languages (POPL), pp. 373\u2013384. ACM (2014)","DOI":"10.1145\/2578855.2535845"},{"key":"11_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1007\/978-3-642-39799-8_9","volume-title":"Computer Aided Verification","author":"J Alglave","year":"2013","unstructured":"Alglave, J., Kroening, D., Tautschnig, M.: Partial orders for efficient bounded model checking of\u00a0concurrent\u00a0software. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 141\u2013157. Springer, Heidelberg (2013). doi:10.1007\/978-3-642-39799-8_9"},{"key":"11_CR3","unstructured":"Carre, J.-L., Hymans, C.: From single-thread to multithreaded: an efficient static analysis algorithm. arXiv:0910.5833[cs], October 2009"},{"key":"11_CR4","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R., Logozzo, F.: A parametric segmentation functor for fully automatic and scalable array content analysis. In: Principles of Programming Languages (POPL), pp. 105\u2013118. ACM (2011)","DOI":"10.1145\/1925844.1926399"},{"key":"11_CR5","doi-asserted-by":"publisher","first-page":"285","DOI":"10.1023\/A:1014746130920","volume":"20","author":"J Esparza","year":"2002","unstructured":"Esparza, J., R\u00f6mer, S., Vogler, W.: An improvement of McMillan\u2019s unfolding algorithm. Formal Methods Syst. Des. 20, 285\u2013310 (2002)","journal-title":"Formal Methods Syst. Des."},{"key":"11_CR6","doi-asserted-by":"crossref","unstructured":"Farzan, A., Holzer, A., Razavi, N., Veith, H.: Con2Colic testing. In: Foundations of Software Engineering (FSE), pp. 37\u201347. ACM (2013)","DOI":"10.1145\/2491411.2491453"},{"key":"11_CR7","doi-asserted-by":"crossref","unstructured":"Farzan, A., Kincaid, Z.: Verification of parameterized concurrent programs by modular reasoning about data and control. In: Principles of Programming Languages (POPL), pp. 297\u2013308. ACM (2012)","DOI":"10.1145\/2103621.2103693"},{"key":"11_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1007\/978-3-540-71209-1_10","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Farzan","year":"2007","unstructured":"Farzan, A., Madhusudan, P.: Causal dataflow analysis for concurrent programs. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 102\u2013116. Springer, Heidelberg (2007). doi:10.1007\/978-3-540-71209-1_10"},{"key":"11_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/3-540-44829-2_14","volume-title":"Model Checking Software","author":"C Flanagan","year":"2003","unstructured":"Flanagan, C., Qadeer, S.: Thread-modular model checking. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol. 2648, pp. 213\u2013224. Springer, Heidelberg (2003). doi:10.1007\/3-540-44829-2_14"},{"key":"11_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60761-7","volume-title":"Partial-Order Methods for the Verification of Concurrent Systems","year":"1996","unstructured":"Godefroid, P. (ed.): Partial-Order Methods for the Verification of Concurrent Systems. LNCS, vol. 1032. Springer, Heidelberg (1996). doi:10.1007\/3-540-60761-7"},{"key":"11_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/978-3-319-52234-0_14","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"H G\u00fcnther","year":"2017","unstructured":"G\u00fcnther, H., Laarman, A., Sokolova, A., Weissenbacher, G.: Dynamic reductions for model checking concurrent software. In: Bouajjani, A., Monniaux, D. (eds.) VMCAI 2017. LNCS, vol. 10145, pp. 246\u2013265. Springer, Cham (2017). doi:10.1007\/978-3-319-52234-0_14"},{"key":"11_CR12","doi-asserted-by":"crossref","unstructured":"Hoenicke, J., Majumdar, R., Podelski, A.: Thread modularity at many levels: a pearl in compositional verification. In: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, pp. 473\u2013485. ACM, New York (2017)","DOI":"10.1145\/3009837.3009893"},{"issue":"2","key":"11_CR13","doi-asserted-by":"publisher","first-page":"285","DOI":"10.1007\/s10270-012-0230-7","volume":"12","author":"B Jeannet","year":"2012","unstructured":"Jeannet, B.: Relational interprocedural verification of concurrent programs. Softw. Syst. Model. 12(2), 285\u2013306 (2012)","journal-title":"Softw. Syst. Model."},{"key":"11_CR14","first-page":"1","volume":"22","author":"K K\u00e4hk\u00e4nen","year":"2014","unstructured":"K\u00e4hk\u00e4nen, K., Saarikivi, O., Heljanko, K.: Unfolding based automated testing of multithreaded programs. Autom. Softw. Eng. 22, 1\u201341 (2014)","journal-title":"Autom. Softw. Eng."},{"key":"11_CR15","doi-asserted-by":"crossref","unstructured":"Kusano, M., Wang, C.: Flow-sensitive composition of thread-modular abstract interpretation. In: Foundations of Software Engineering (FSE), pp. 799\u2013809. ACM (2016)","DOI":"10.1145\/2950290.2950291"},{"key":"11_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"218","DOI":"10.1007\/978-3-540-74061-2_14","volume-title":"Static Analysis","author":"A Malkis","year":"2007","unstructured":"Malkis, A., Podelski, A., Rybalchenko, A.: Precise thread-modular verification. In: Nielson, H.R., Fil\u00e9, G. (eds.) SAS 2007. LNCS, vol. 4634, pp. 218\u2013232. Springer, Heidelberg (2007). doi:10.1007\/978-3-540-74061-2_14"},{"key":"11_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"164","DOI":"10.1007\/3-540-56496-9_14","volume-title":"Computer Aided Verification","author":"KL McMillan","year":"1993","unstructured":"McMillan, K.L.: Using unfoldings to avoid the state explosion problem in the verification of asynchronous circuits. In: Bochmann, G., Probst, D.K. (eds.) CAV 1992. LNCS, vol. 663, pp. 164\u2013177. Springer, Heidelberg (1993). doi:10.1007\/3-540-56496-9_14"},{"key":"11_CR18","doi-asserted-by":"crossref","unstructured":"Min\u00e9, A.: Static analysis of run-time errors in embedded real-time parallel C programs. Log. Methods Comput. Sci. 8(1) (2012)","DOI":"10.2168\/LMCS-8(1:26)2012"},{"key":"11_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/978-3-642-54013-4_3","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A Min\u00e9","year":"2014","unstructured":"Min\u00e9, A.: Relational thread-modular static value analysis by abstract interpretation. In: McMillan, K.L., Rival, X. (eds.) VMCAI 2014. LNCS, vol. 8318, pp. 39\u201358. Springer, Heidelberg (2014). doi:10.1007\/978-3-642-54013-4_3"},{"key":"11_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"386","DOI":"10.1007\/978-3-319-52234-0_21","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"R Monat","year":"2017","unstructured":"Monat, R., Min\u00e9, A.: Precise thread-modular abstract interpretation of concurrent programs using relational interference abstractions. In: Bouajjani, A., Monniaux, D. (eds.) VMCAI 2017. LNCS, vol. 10145, pp. 386\u2013404. Springer, Cham (2017). doi:10.1007\/978-3-319-52234-0_21"},{"issue":"1","key":"11_CR21","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1016\/0304-3975(81)90112-2","volume":"13","author":"M Nielsen","year":"1981","unstructured":"Nielsen, M., Plotkin, G., Winskel, G.: Petri nets, event structures and domains, part I. Theoret. Comput. Sci. 13(1), 85\u2013108 (1981)","journal-title":"Theoret. Comput. Sci."},{"key":"11_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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. 697, pp. 409\u2013423. Springer, Heidelberg (1993). doi:10.1007\/3-540-56922-7_34"},{"key":"11_CR23","unstructured":"Rodr\u00e9guez, C., Sousa, M., Sharma, S., Kroening, D.: Unfolding-based partial order reduction. In: Concurrency Theory (CONCUR). LIPIcs, vol. 42, pp. 456\u2013469. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2015)"},{"key":"11_CR24","doi-asserted-by":"crossref","unstructured":"Sousa, M., Rodr\u00e9guez, C., D\u2019Silva, V., Kroening, D.: Abstract interpretation with unfoldings. CoRR abs\/1705.00595 (2017)","DOI":"10.1007\/978-3-319-63390-9_11"},{"key":"11_CR25","doi-asserted-by":"crossref","unstructured":"Wachter, B., Kroening, D., Ouaknine, J.: Verifying multi-threaded software with impact. In: Formal Methods in Computer-Aided Design (FMCAD), pp. 210\u2013217 (2013)","DOI":"10.1109\/FMCAD.2013.6679412"},{"key":"11_CR26","unstructured":"Yakobowski, B., Bonichon, R.: Frama-C\u2019s Mthread plug-in. Report, Software Reliability Laboratory (2012)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-63390-9_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,7,30]],"date-time":"2022-07-30T20:25:50Z","timestamp":1659212750000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-63390-9_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319633893","9783319633909"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-63390-9_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]},"assertion":[{"value":"13 July 2017","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Heidelberg","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2017","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 July 2017","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 July 2017","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2017","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/cavconference.org\/2017\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}