{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:15:36Z","timestamp":1767928536677,"version":"3.49.0"},"publisher-location":"Cham","reference-count":23,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030670665","type":"print"},{"value":"9783030670672","type":"electronic"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"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":[[2021]]},"DOI":"10.1007\/978-3-030-67067-2_9","type":"book-chapter","created":{"date-parts":[[2021,1,11]],"date-time":"2021-01-11T20:57:20Z","timestamp":1610398640000},"page":"174-195","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":10,"title":["Verification of Concurrent Programs Using Petri Net Unfoldings"],"prefix":"10.1007","author":[{"given":"Daniel","family":"Dietsch","sequence":"first","affiliation":[]},{"given":"Matthias","family":"Heizmann","sequence":"additional","affiliation":[]},{"given":"Dominik","family":"Klumpp","sequence":"additional","affiliation":[]},{"given":"Mehdi","family":"Naouar","sequence":"additional","affiliation":[]},{"given":"Andreas","family":"Podelski","sequence":"additional","affiliation":[]},{"given":"Claus","family":"Sch\u00e4tzle","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,1,12]]},"reference":[{"key":"9_CR1","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 concurrent software. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 141\u2013157. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_9"},{"key":"9_CR2","doi-asserted-by":"publisher","unstructured":"Apt, K.R., de\u00a0Boer, F.S., Olderog, E.R.: Verification of Sequential and Concurrent Programs. Springer Science & Business Media, Verlag (2009). https:\/\/doi.org\/10.1007\/978-1-84882-745-5","DOI":"10.1007\/978-1-84882-745-5"},{"key":"9_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"399","DOI":"10.1007\/978-3-540-70545-1_37","volume-title":"Computer Aided Verification","author":"J Berdine","year":"2008","unstructured":"Berdine, J., Lev-Ami, T., Manevich, R., Ramalingam, G., Sagiv, M.: Thread quantification for concurrent shape analysis. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 399\u2013413. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-70545-1_37"},{"issue":"1","key":"9_CR4","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10009-017-0469-y","volume":"21","author":"D Beyer","year":"2017","unstructured":"Beyer, D., L\u00f6we, S., Wendler, P.: Reliable benchmarking: requirements and solutions. Int. J. Softw. Tools Technol. Transf. 21(1), 1\u201329 (2017). https:\/\/doi.org\/10.1007\/s10009-017-0469-y","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"9_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/978-3-662-48899-7_17","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"F Cassez","year":"2015","unstructured":"Cassez, F., Ziegler, F.: Verification of concurrent programs using trace abstraction refinement. In: Davis, M., Fehnker, A., McIver, A., Voronkov, A. (eds.) LPAR 2015. LNCS, vol. 9450, pp. 233\u2013248. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-48899-7_17"},{"key":"9_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-319-13338-6_14","volume-title":"Hardware and Software: Verification and Testing","author":"D-H Chu","year":"2014","unstructured":"Chu, D.-H., Jaffar, J.: A framework to synergize partial order reduction with state interpolation. In: Yahav, E. (ed.) HVC 2014. LNCS, vol. 8855, pp. 171\u2013187. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-13338-6_14"},{"key":"9_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1007\/978-3-642-22110-1_28","volume-title":"Computer Aided Verification","author":"A Donaldson","year":"2011","unstructured":"Donaldson, A., Kaiser, A., Kroening, D., Wahl, T.: Symmetry-aware predicate abstraction for shared-variable concurrent programs. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 356\u2013371. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_28"},{"key":"9_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/978-3-642-12002-2_22","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K Dr\u00e4ger","year":"2010","unstructured":"Dr\u00e4ger, K., Kupriyanov, A., Finkbeiner, B., Wehrheim, H.: SLAB: a certifying model checker for infinite-state concurrent systems. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 271\u2013274. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-12002-2_22"},{"issue":"3","key":"9_CR9","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(3), 285\u2013310 (2002). https:\/\/doi.org\/10.1023\/A:1014746130920","journal-title":"Formal Methods Syst. Des."},{"issue":"1","key":"9_CR10","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1145\/2103621.2103693","volume":"47","author":"A Farzan","year":"2012","unstructured":"Farzan, A., Kincaid, Z.: Verification of parameterized concurrent programs by modular reasoning about data and control. ACM SIGPLAN Not. 47(1), 297\u2013308 (2012)","journal-title":"ACM SIGPLAN Not."},{"issue":"1","key":"9_CR11","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1145\/2480359.2429086","volume":"48","author":"A Farzan","year":"2013","unstructured":"Farzan, A., Kincaid, Z., Podelski, A.: Inductive data flow graphs. ACM SIGPLAN Not. 48(1), 129\u2013142 (2013)","journal-title":"ACM SIGPLAN Not."},{"key":"9_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/978-3-030-25540-4_11","volume-title":"Computer Aided Verification","author":"A Farzan","year":"2019","unstructured":"Farzan, A., Vandikas, A.: Automated hypersafety verification. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11561, pp. 200\u2013218. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_11"},{"issue":"POPL","key":"9_CR13","doi-asserted-by":"publisher","first-page":"13:1","DOI":"10.1145\/3371081","volume":"4","author":"A Farzan","year":"2020","unstructured":"Farzan, A., Vandikas, A.: Reductions for safety proofs. Proc. ACM Program. Lang. 4(POPL), 13:1\u201313:28 (2020)","journal-title":"Proc. ACM Program. Lang."},{"key":"9_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1007\/978-3-030-25540-4_19","volume-title":"Computer Aided Verification","author":"N Gavrilenko","year":"2019","unstructured":"Gavrilenko, N., Ponce-de-Le\u00f3n, H., Furbach, F., Heljanko, K., Meyer, R.: BMC for weak memory models: relation analysis for compact SMT encodings. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11561, pp. 355\u2013365. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_19"},{"key":"9_CR15","doi-asserted-by":"crossref","unstructured":"Gupta, A., Popeea, C., Rybalchenko, A.: Predicate abstraction and refinement for verifying multi-threaded programs. In: Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 331\u2013344. ACM (2011)","DOI":"10.1145\/1926385.1926424"},{"key":"9_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1007\/978-3-642-39799-8_2","volume-title":"Computer Aided Verification","author":"M Heizmann","year":"2013","unstructured":"Heizmann, M., Hoenicke, J., Podelski, A.: Software model checking for people who love automata. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 36\u201352. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_2"},{"key":"9_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"262","DOI":"10.1007\/978-3-540-45069-6_27","volume-title":"Computer Aided Verification","author":"TA Henzinger","year":"2003","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Qadeer, S.: Thread-modular abstraction refinement. In: Hunt, W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 262\u2013274. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-45069-6_27"},{"key":"9_CR18","doi-asserted-by":"crossref","unstructured":"Inverso, O., Trubiani, C.: Parallel and distributed bounded model checking of multi-threaded programs. In: Proceedings of the 25th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, pp. 202\u2013216. ACM (2020)","DOI":"10.1145\/3332466.3374529"},{"key":"9_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1007\/978-3-642-00768-2_12","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"V Kahlon","year":"2009","unstructured":"Kahlon, V., Sankaranarayanan, S., Gupta, A.: Semantic reduction of thread interleavings in concurrent programs. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 124\u2013138. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-00768-2_12"},{"key":"9_CR20","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: von Bochmann, G., Probst, D.K. (eds.) CAV 1992. LNCS, vol. 663, pp. 164\u2013177. Springer, Heidelberg (1993). https:\/\/doi.org\/10.1007\/3-540-56496-9_14"},{"key":"9_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"398","DOI":"10.1007\/978-3-642-19718-5_21","volume-title":"Programming Languages and Systems","author":"A Min\u00e9","year":"2011","unstructured":"Min\u00e9, A.: Static analysis of run-time errors in embedded critical parallel C programs. In: Barthe, G. (ed.) ESOP 2011. LNCS, vol. 6602, pp. 398\u2013418. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-19718-5_21"},{"key":"9_CR22","doi-asserted-by":"crossref","unstructured":"Wachter, B., Kroening, D., Ouaknine, J.: Verifying multi-threaded software with Impact. In: Formal Methods in Computer-Aided Design, pp. 210\u2013217. IEEE (2013)","DOI":"10.1109\/FMCAD.2013.6679412"},{"issue":"5","key":"9_CR23","doi-asserted-by":"publisher","first-page":"549","DOI":"10.1109\/TSE.2018.2864122","volume":"46","author":"L Yin","year":"2020","unstructured":"Yin, L., Dong, W., Liu, W., Wang, J.: On scheduling constraint abstraction for multi-threaded program verification. IEEE Trans. Softw. Eng. 46(5), 549\u2013565 (2020)","journal-title":"IEEE Trans. Softw. Eng."}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-67067-2_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,6,10]],"date-time":"2024-06-10T20:10:38Z","timestamp":1718050238000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-67067-2_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030670665","9783030670672"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-67067-2_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"12 January 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"VMCAI","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Verification, Model Checking, and Abstract Interpretation","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Copenhagen","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Denmark","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17 January 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"19 January 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"vmcai2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/popl21.sigplan.org\/home\/VMCAI-2021","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"48","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"22","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"1","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"46% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3,1","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"4,6","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The conference took place virtually due to the COVID-19 pandemic.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}