{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T14:05:50Z","timestamp":1743084350975,"version":"3.40.3"},"publisher-location":"Cham","reference-count":19,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030910136"},{"type":"electronic","value":"9783030910143"}],"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-91014-3_12","type":"book-chapter","created":{"date-parts":[[2021,12,1]],"date-time":"2021-12-01T10:03:39Z","timestamp":1638353019000},"page":"169-186","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Separating Map Variables in a Logic-Based Intermediate Verification Language"],"prefix":"10.1007","author":[{"given":"Daniel","family":"Dietsch","sequence":"first","affiliation":[]},{"given":"Matthias","family":"Heizmann","sequence":"additional","affiliation":[]},{"given":"Jochen","family":"Hoenicke","sequence":"additional","affiliation":[]},{"given":"Alexander","family":"Nutz","sequence":"additional","affiliation":[]},{"given":"Andreas","family":"Podelski","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,12,2]]},"reference":[{"key":"12_CR1","doi-asserted-by":"crossref","unstructured":"Beyer, D., Henzinger, T.A., Majumdar, R., Rybalchenko, A.: Path invariants. In: PLDI, pp. 300\u2013309. ACM (2007)","DOI":"10.1145\/1273442.1250769"},{"key":"12_CR2","doi-asserted-by":"crossref","unstructured":"Carter, M., He, S., Whitaker, J., Rakamaric, Z., Emmi, M.: SMACK software verification toolchain. In: ICSE (Companion Volume), pp. 589\u2013592. ACM (2016)","DOI":"10.1145\/2889160.2889163"},{"key":"12_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"452","DOI":"10.1007\/978-3-319-89963-3_31","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Dietsch","year":"2018","unstructured":"Dietsch, D., et al.: Ultimate taipan with dynamic block encoding - (competition contribution). In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10806, pp. 452\u2013456. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89963-3_31"},{"key":"12_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1007\/978-3-030-03592-1_17","volume-title":"Verified Software. Theories, Tools, and Experiments","author":"D Dietsch","year":"2018","unstructured":"Dietsch, D., Heizmann, M., Hoenicke, J., Nutz, A., Podelski, A.: The map equality domain. In: Piskac, R., R\u00fcmmer, P. (eds.) VSTTE 2018. LNCS, vol. 11294, pp. 291\u2013308. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-03592-1_17"},{"key":"12_CR5","unstructured":"Dietsch, D., Heizmann, M., Hoenicke, J., Nutz, A., Podelski, A.: Different maps for different uses. A program transformation for intermediate verification languages. CoRR, abs\/1901.01915 (2019)"},{"issue":"1","key":"12_CR6","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/BF01407931","volume":"20","author":"P Feautrier","year":"1991","unstructured":"Feautrier, P.: Dataflow analysis of array and scalar references. Int. J. Parallel Prog. 20(1), 23\u201353 (1991)","journal-title":"Int. J. Parallel Prog."},{"key":"12_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1007\/978-3-319-66706-5_7","volume-title":"Static Analysis","author":"M Greitschus","year":"2017","unstructured":"Greitschus, M., Dietsch, D., Podelski, A.: Loop invariants from counterexamples. In: Ranzato, F. (ed.) SAS 2017. LNCS, vol. 10422, pp. 128\u2013147. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66706-5_7"},{"key":"12_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1007\/978-3-662-46681-0_41","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Gurfinkel","year":"2015","unstructured":"Gurfinkel, A., Kahsai, T., Navas, J.A.: SeaHorn: a framework for verifying C programs (competition contribution). In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 447\u2013450. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_41"},{"key":"12_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"148","DOI":"10.1007\/978-3-319-66706-5_8","volume-title":"Static Analysis","author":"A Gurfinkel","year":"2017","unstructured":"Gurfinkel, A., Navas, J.A.: A context-sensitive memory model for verification of C\/C++ programs. In: Ranzato, F. (ed.) SAS 2017. LNCS, vol. 10422, pp. 148\u2013168. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66706-5_8"},{"key":"12_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1007\/978-3-319-89963-3_30","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M Heizmann","year":"2018","unstructured":"Heizmann, M., et al.: Ultimate automizer and the search for perfect interpolants. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10806, pp. 447\u2013451. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89963-3_30"},{"key":"12_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"352","DOI":"10.1007\/978-3-319-41528-4_19","volume-title":"Computer Aided Verification","author":"T Kahsai","year":"2016","unstructured":"Kahsai, T., R\u00fcmmer, P., Sanchez, H., Sch\u00e4f, M.: JayHorn: a framework for verifying Java programs. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 352\u2013358. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41528-4_19"},{"key":"12_CR12","unstructured":"Leino, K.R.M.: This is boogie 2. Technical report, Microsoft Research (2008). https:\/\/www.microsoft.com\/en-us\/research\/publication\/this-is-boogie-2-2\/"},{"key":"12_CR13","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/978-3-642-17511-4_20","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"KRM Leino","year":"2010","unstructured":"Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010. LNCS (LNAI), vol. 6355, pp. 348\u2013370. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-17511-4_20"},{"key":"12_CR14","unstructured":"McCarthy, J.: Towards a mathematical science of computation. In: IFIP Congress, pp. 21\u201328 (1962)"},{"key":"12_CR15","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-03811-6","volume-title":"Principles of Program Analysis","author":"F Nielson","year":"1999","unstructured":"Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis. Springer, Heidelberg (1999)"},{"issue":"1","key":"12_CR16","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1145\/509705.509708","volume":"24","author":"Y Paek","year":"2002","unstructured":"Paek, Y., Hoeflinger, J., Padua, D.A.: Efficient and precise array access analysis. ACM Trans. Program. Lang. Syst. 24(1), 65\u2013109 (2002)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"12_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"546","DOI":"10.1007\/3-540-57659-2_31","volume-title":"Languages and Compilers for Parallel Computing","author":"W Pugh","year":"1994","unstructured":"Pugh, W., Wonnacott, D.: An exact method for analysis of value-based array data dependences. In: Banerjee, U., Gelernter, D., Nicolau, A., Padua, D. (eds.) LCPC 1993. LNCS, vol. 768, pp. 546\u2013566. Springer, Heidelberg (1994). https:\/\/doi.org\/10.1007\/3-540-57659-2_31"},{"key":"12_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"290","DOI":"10.1007\/978-3-540-93900-9_24","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"Z Rakamari\u0107","year":"2008","unstructured":"Rakamari\u0107, Z., Hu, A.J.: A scalable memory model for low-level code. In: Jones, N.D., M\u00fcller-Olm, M. (eds.) VMCAI 2009. LNCS, vol. 5403, pp. 290\u2013304. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-93900-9_24"},{"key":"12_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"539","DOI":"10.1007\/978-3-319-52234-0_29","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"W Wang","year":"2017","unstructured":"Wang, W., Barrett, C., Wies, T.: Partitioned memory models for program analysis. In: Bouajjani, A., Monniaux, D. (eds.) VMCAI 2017. LNCS, vol. 10145, pp. 539\u2013558. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-52234-0_29"}],"container-title":["Lecture Notes in Computer Science","Networked Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-91014-3_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,12,1]],"date-time":"2021-12-01T10:05:16Z","timestamp":1638353116000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-91014-3_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030910136","9783030910143"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-91014-3_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"2 December 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"NETYS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Networked Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"19 May 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21 May 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"netys2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/netys.net\/","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":"32","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":"15","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":"2","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":"47% - 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","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":"2,84","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":"No","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}