{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,11]],"date-time":"2024-09-11T11:14:01Z","timestamp":1726053241314},"publisher-location":"Cham","reference-count":31,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030309220"},{"type":"electronic","value":"9783030309237"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-30923-7_5","type":"book-chapter","created":{"date-parts":[[2019,10,1]],"date-time":"2019-10-01T23:04:08Z","timestamp":1569971048000},"page":"74-93","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["String Abstraction for Model Checking of C Programs"],"prefix":"10.1007","author":[{"given":"Agostino","family":"Cortesi","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Henrich","family":"Lauko","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Martina","family":"Olliaro","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Petr","family":"Ro\u010dkai","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,10,2]]},"reference":[{"key":"5_CR1","unstructured":"Polyspace, MathWorks (2001)"},{"key":"5_CR2","unstructured":"Static Code Analysis, OWASP (2017)"},{"key":"5_CR3","unstructured":"Interactive: the top programming languages 2018. IEEE Spectrum Magazine (2018)"},{"issue":"4","key":"5_CR4","doi-asserted-by":"publisher","first-page":"297","DOI":"10.3233\/FI-2018-1650","volume":"158","author":"R Amadini","year":"2018","unstructured":"Amadini, R., et al.: Reference abstract domains and applications to string analysis. Fundam. Inform. 158(4), 297\u2013326 (2018)","journal-title":"Fundam. Inform."},{"key":"5_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/978-3-662-54577-5_3","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R Amadini","year":"2017","unstructured":"Amadini, R., et al.: Combining string abstract domains for JavaScript analysis: an evaluation. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10205, pp. 41\u201357. Springer, Heidelberg (2017). \n                    https:\/\/doi.org\/10.1007\/978-3-662-54577-5_3"},{"key":"5_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1007\/978-3-319-68167-2_14","volume-title":"Automated Technology for Verification and Analysis","author":"Z Baranov\u00e1","year":"2017","unstructured":"Baranov\u00e1, Z., et al.: Model checking of C and C++ with DIVINE 4. In: D\u2019Souza, D., Narayan Kumar, K. (eds.) ATVA 2017. LNCS, vol. 10482, pp. 201\u2013207. Springer, Cham (2017). \n                    https:\/\/doi.org\/10.1007\/978-3-319-68167-2_14"},{"key":"5_CR7","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-68670-7","volume-title":"String Analysis for Software Verification and Security","author":"T Bultan","year":"2017","unstructured":"Bultan, T., Yu, F., Alkhalaf, M., Aydin, A.: String Analysis for Software Verification and Security. Springer, Cham (2017). \n                    https:\/\/doi.org\/10.1007\/978-3-319-68670-7"},{"key":"5_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-44898-5_1","volume-title":"Static Analysis","author":"AS Christensen","year":"2003","unstructured":"Christensen, A.S., M\u00f8ller, A., Schwartzbach, M.I.: Precise analysis of string expressions. In: Cousot, R. (ed.) SAS 2003. LNCS, vol. 2694, pp. 1\u201318. Springer, Heidelberg (2003). \n                    https:\/\/doi.org\/10.1007\/3-540-44898-5_1"},{"issue":"5","key":"5_CR9","doi-asserted-by":"publisher","first-page":"1512","DOI":"10.1145\/186025.186051","volume":"16","author":"EM Clarke","year":"1994","unstructured":"Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. ACM Trans. Program. Lang. Syst. 16(5), 1512\u20131542 (1994)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"5_CR10","doi-asserted-by":"crossref","unstructured":"Cortesi, A., Olliaro, M.: M-string segmentation: a refined abstract domain for string analysis in C programs. In: Proceedings of the 12th International Symposium on Theoretical Aspects of Software Engineering, TASE 2018, Guangzhou, China, 29\u201331 August 2018 (2018)","DOI":"10.1109\/TASE.2018.00009"},{"issue":"2","key":"5_CR11","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1002\/spe.2218","volume":"45","author":"G Costantini","year":"2015","unstructured":"Costantini, G., Ferrara, P., Cortesi, A.: A suite of abstract domains for static analysis of string values. Softw. Pract. Exp. 45(2), 245\u2013287 (2015)","journal-title":"Softw. Pract. Exp."},{"key":"5_CR12","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Conference Record of the Fourth ACM Symposium on Principles of Programming Languages, Los Angeles, California, USA, January 1977, pp. 238\u2013252 (1977)","DOI":"10.1145\/512950.512973"},{"key":"5_CR13","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R., Logozzo, F.: A parametric segmentation functor for fully automatic and scalable array content analysis. In: Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, Austin, TX, USA, 26\u201328 January 2011, pp. 105\u2013118 (2011)","DOI":"10.1145\/1926385.1926399"},{"key":"5_CR14","doi-asserted-by":"crossref","unstructured":"Dor, N., Rodeh, M., Sagiv, S.: CSSV: towards a realistic tool for statically detecting all buffer overflows in C. In: Proceedings of the ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation 2003, San Diego, California, USA, 9\u201311 June 2003, pp. 155\u2013167 (2003)","DOI":"10.1145\/781131.781149"},{"issue":"7","key":"5_CR15","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 Trans. CAD Integr. Circ. Syst. 27(7), 1165\u20131178 (2008)","journal-title":"IEEE Trans. CAD Integr. Circ. Syst."},{"issue":"1","key":"5_CR16","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1109\/52.976940","volume":"19","author":"D Evans","year":"2002","unstructured":"Evans, D., Larochelle, D.: Improving security using extensible lightweight static analysis. IEEE Softw. 19(1), 42\u201351 (2002)","journal-title":"IEEE Softw."},{"key":"5_CR17","unstructured":"Holzmann, G.J.: Static source code checking for user-defined properties. In: Integrated Design and Process Technology, IDPT 2002. Society for Design and Process Science, Pasadena (2002)"},{"key":"5_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"238","DOI":"10.1007\/978-3-642-03237-0_17","volume-title":"Static Analysis","author":"SH Jensen","year":"2009","unstructured":"Jensen, S.H., M\u00f8ller, A., Thiemann, P.: Type analysis for JavaScript. In: Palsberg, J., Su, Z. (eds.) SAS 2009. LNCS, vol. 5673, pp. 238\u2013255. Springer, Heidelberg (2009). \n                    https:\/\/doi.org\/10.1007\/978-3-642-03237-0_17"},{"key":"5_CR19","unstructured":"Jones, R.W.M., Kelly, P.H.J.: Backwards-compatible bounds checking for arrays and pointers in C programs. In: AADEBUG, pp. 13\u201326 (1997)"},{"key":"5_CR20","doi-asserted-by":"crossref","unstructured":"Kashyap, V., et al.: JSAI: a static analysis platform for JavaScript. In: Proceedings of the 22nd ACM SIGSOFT International Symposium on Foundations of Software Engineering, (FSE-22), Hong Kong, China, 16\u201322 November 2014, pp. 121\u2013132 (2014)","DOI":"10.1145\/2635868.2635904"},{"key":"5_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"372","DOI":"10.1007\/978-3-319-12736-1_20","volume-title":"Programming Languages and Systems","author":"S-W Kim","year":"2014","unstructured":"Kim, S.-W., Chin, W., Park, J., Kim, J., Ryu, S.: Inferring grammatical summaries of string values. In: Garrigue, J. (ed.) APLAS 2014. LNCS, vol. 8858, pp. 372\u2013391. Springer, Cham (2014). \n                    https:\/\/doi.org\/10.1007\/978-3-319-12736-1_20"},{"key":"5_CR22","unstructured":"Lattner, C., Adve, V.: LLVM: a compilation framework for lifelong program analysis & transformation. In: International Symposium on Code Generation and Optimization (CGO 2004), Palo Alto, California, March 2004"},{"key":"5_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"313","DOI":"10.1007\/978-3-030-02508-3_17","volume-title":"Theoretical Aspects of Computing \u2013 ICTAC 2018","author":"H Lauko","year":"2018","unstructured":"Lauko, H., Ro\u010dkai, P., Barnat, J.: Symbolic computation via program transformation. In: Fischer, B., Uustalu, T. (eds.) ICTAC 2018. LNCS, vol. 11187, pp. 313\u2013332. Springer, Cham (2018). \n                    https:\/\/doi.org\/10.1007\/978-3-030-02508-3_17"},{"key":"5_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1007\/978-3-642-54807-9_12","volume-title":"Compiler Construction","author":"M Madsen","year":"2014","unstructured":"Madsen, M., Andreasen, E.: String analysis for dynamic field access. In: Cohen, A. (ed.) CC 2014. LNCS, vol. 8409, pp. 197\u2013217. Springer, Heidelberg (2014). \n                    https:\/\/doi.org\/10.1007\/978-3-642-54807-9_12"},{"key":"5_CR25","unstructured":"One, A.: Smashing the stack for fun and profit. Phrack 7(49) (1996 ). \n                    http:\/\/www.phrack.com\/issues.html?issue=49&id=14"},{"key":"5_CR26","doi-asserted-by":"crossref","unstructured":"Park, C., Im, H., Ryu, S.: Precise and scalable static analysis of jQuery using a regular expression domain. In: Proceedings of the 12th Symposium on Dynamic Languages, DLS 2016, Amsterdam, The Netherlands, 1 November 2016, pp. 25\u201336 (2016)","DOI":"10.1145\/2989225.2989228"},{"key":"5_CR27","doi-asserted-by":"crossref","unstructured":"Shahriar, H., Zulkernine, M.: Classification of static analysis-based buffer overflow detectors. In: Fourth International Conference on Secure Software Integration and Reliability Improvement, SSIRI 2010, Singapore, 9\u201311 June 2010, Companion Volume, pp. 94\u2013101 (2010)","DOI":"10.1109\/SSIRI-C.2010.28"},{"key":"5_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/978-3-662-53413-7_3","volume-title":"Static Analysis","author":"F Spoto","year":"2016","unstructured":"Spoto, F.: The julia static analyzer for Java. In: Rival, X. (ed.) SAS 2016. LNCS, vol. 9837, pp. 39\u201357. Springer, Heidelberg (2016). \n                    https:\/\/doi.org\/10.1007\/978-3-662-53413-7_3"},{"key":"5_CR29","unstructured":"Wagner, D.A., Foster, J.S., Brewer, E.A., Aiken, A.: A first step towards automated detection of buffer overrun vulnerabilities. In: Proceedings of the Network and Distributed System Security Symposium, NDSS, San Diego, California, USA, p. 2000 (2000)"},{"key":"5_CR30","doi-asserted-by":"crossref","unstructured":"Xie, Y., Chou, A., Engler, D.R.: ARCHER: using symbolic, path-sensitive analysis to detect memory access errors. In: Proceedings of the 11th ACM SIGSOFT Symposium on Foundations of Software Engineering 2003 Held Jointly with 9th European Software Engineering Conference, ESEC\/FSE 2003, Helsinki, Finland, 1\u20135 September 2003, pp. 327\u2013336 (2003)","DOI":"10.1145\/949952.940115"},{"key":"5_CR31","doi-asserted-by":"crossref","unstructured":"Xu, R-G., Godefroid, P., Majumdar, R.: Testing for buffer overflows with length abstraction. In: Proceedings of the ACM\/SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2008, Seattle, WA, USA, 20\u201324 July 2008, pp. 27\u201338 (2008)","DOI":"10.1145\/1390630.1390636"}],"container-title":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-30923-7_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,1]],"date-time":"2019-10-01T23:25:40Z","timestamp":1569972340000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-30923-7_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030309220","9783030309237"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-30923-7_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"2 October 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SPIN","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Model Checking Software","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Beijing","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"China","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15 July 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"19 July 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"spin2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conf.researchr.org\/track\/spin-2019\/spin-2019-papers","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":"29","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":"13","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":"0","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":"45% - 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":"0","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)"}}]}}