{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,12]],"date-time":"2024-09-12T05:30:49Z","timestamp":1726119049072},"publisher-location":"Cham","reference-count":28,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030714994"},{"type":"electronic","value":"9783030715007"}],"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:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,3,20]],"date-time":"2021-03-20T00:00:00Z","timestamp":1616198400000},"content-version":"vor","delay-in-days":78,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,3,20]],"date-time":"2021-03-20T00:00:00Z","timestamp":1616198400000},"content-version":"vor","delay-in-days":78,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"abstract":"Abstract<\/jats:title>Software model checkers are able to exhaustively explore different bounded program executions arising from various sources of non-determinism. These tools provide statements to produce non-deterministic values for certain variables, thus forcing the corresponding model checker to considerall<\/jats:italic>possible values for these during verification. While these statements offer an effective way of verifying programs handling basic data types and simple structured types, they are inappropriate as a mechanism for nondeterministic generation of pointers, favoring the use of insertion routines to produce dynamic data structures when verifying, via model checking, programs handling such data types.<\/jats:p>We present a technique to improve model checking of programs handling heap-allocated data types, by taming the explosion of candidate structures that can be built when non-deterministically initializing heap object fields. The technique exploits precomputedrelational bounds<\/jats:italic>, that disregard values deemed invalid by the structure\u2019s type invariant, thus reducing the state space to be explored by the model checker. Precomputing the relational bounds is a challenging costly task too, for which we also present an efficient algorithm, based on incremental SAT solving.<\/jats:p>We implement our approach on top of the bounded model checker, and show that, for a number of data structures implementations, we can handle significantly larger input structures and detect faults that is unable to detect.<\/jats:p>","DOI":"10.1007\/978-3-030-71500-7_11","type":"book-chapter","created":{"date-parts":[[2021,3,19]],"date-time":"2021-03-19T09:12:14Z","timestamp":1616145134000},"page":"218-239","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Efficient Bounded Model Checking of Heap-Manipulating Programs using Tight Field Bounds"],"prefix":"10.1007","author":[{"given":"Pablo","family":"Ponzio","sequence":"first","affiliation":[]},{"given":"Ariel","family":"Godio","sequence":"additional","affiliation":[]},{"given":"Nicol\u00e1s","family":"Rosner","sequence":"additional","affiliation":[]},{"given":"Marcelo","family":"Arroyo","sequence":"additional","affiliation":[]},{"given":"Nazareno","family":"Aguirre","sequence":"additional","affiliation":[]},{"given":"Marcelo F.","family":"Frias","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,3,20]]},"reference":[{"key":"11_CR1","unstructured":"Website and replication package for Efficient Bounded Model Checking of Heap-Manipulating Programs using Tight Field Bounds. https:\/\/sites.google.com\/view\/bmc-bounds."},{"key":"11_CR2","doi-asserted-by":"crossref","unstructured":"Pablo Abad, Nazareno Aguirre, Valeria S. Bengolea, Daniel Alfredo Ciolek, Marcelo F. Frias, Juan P. Galeotti, Tom Maibaum, Mariano M. Moscato, Nicol\u00e1s Rosner, and Ignacio Vissani. Improving test generation under rich contracts by tight bounds and incremental SAT solving. In Sixth IEEE International Conference on Software Testing, Verification and Validation, ICST 2013, Luxembourg, Luxembourg, March 18\u201322, 2013, pages 21\u201330. IEEE Computer Society, 2013.","DOI":"10.1109\/ICST.2013.46"},{"key":"11_CR3","unstructured":"Saswat Anand, Corina S. Pasareanu, and Willem Visser. JPF-SE: A symbolic execution extension to java pathfinder. In Orna Grumberg and Michael Huth, editors, Tools and Algorithms for the Construction and Analysis of Systems, 13th International Conference, TACAS 2007, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2007 Braga, Portugal, March 24 - April 1, 2007, Proceedings, volume 4424 of Lecture Notes in Computer Science, pages 134\u2013138. Springer, 2007."},{"key":"11_CR4","doi-asserted-by":"crossref","unstructured":"Jason Belt, Robby, and Xianghua Deng. Sireum\/topi LDP: a lightweight semi-decision procedure for optimizing symbolic execution-based analyses. In Hans van Vliet and Val\u00e9rie Issarny, editors, Proceedings of the 7th joint meeting of the European Software Engineering Conference and the ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2009, Amsterdam, The Netherlands, August 24\u201328, 2009, pages 355\u2013364. ACM, 2009.","DOI":"10.1145\/1595696.1595762"},{"key":"11_CR5","doi-asserted-by":"crossref","unstructured":"Josh Berdine, Cristiano Calcagno, Byron Cook, Dino Distefano, Peter W. O\u2019Hearn, Thomas Wies, and Hongseok Yang. Shape analysis for composite data structures. In Werner Damm and Holger Hermanns, editors, Computer Aided Verification, 19th International Conference, CAV 2007, Berlin, Germany, July 3\u20137, 2007, Proceedings, volume 4590 of Lecture Notes in Computer Science, pages 178\u2013192. Springer, 2007.","DOI":"10.1007\/978-3-540-73368-3_22"},{"key":"11_CR6","doi-asserted-by":"crossref","unstructured":"Chandrasekhar Boyapati, Sarfraz Khurshid, and Darko Marinov. Korat: automated testing based on java predicates. In Phyllis G. Frankl, editor, Proceedings of the International Symposium on Software Testing and Analysis, ISSTA 2002, Roma, Italy, July 22\u201324, 2002, pages 123\u2013133. ACM, 2002.","DOI":"10.1145\/566171.566191"},{"key":"11_CR7","doi-asserted-by":"crossref","unstructured":"Edmund M. Clarke, Armin Biere, Richard Raimi, and Yunshan Zhu. Bounded model checking using satisfiability solving. Formal Methods Syst. Des., 19(1):7\u201334, 2001.","DOI":"10.1023\/A:1011276507260"},{"key":"11_CR8","unstructured":"Edmund M. Clarke, Daniel Kroening, and Flavio Lerda. A tool for checking ANSI-C programs. In Kurt Jensen and Andreas Podelski, editors, Tools and Algorithms for the Construction and Analysis of Systems, 10th International Conference, TACAS 2004, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2004, Barcelona, Spain, March 29 - April 2, 2004, Proceedings, volume 2988 of Lecture Notes in Computer Science, pages 168\u2013176. Springer, 2004."},{"key":"11_CR9","doi-asserted-by":"crossref","unstructured":"Greg Dennis, Felix Sheng-Ho Chang, and Daniel Jackson. Modular verification of code with SAT. In Lori L. Pollock and Mauro Pezz\u00e8, editors, Proceedings of the ACM\/SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2006, Portland, Maine, USA, July 17\u201320, 2006, pages 109\u2013120. ACM, 2006.","DOI":"10.1145\/1146238.1146251"},{"key":"11_CR10","unstructured":"Niklas E\u00e9n and Niklas S\u00f6rensson. An extensible sat-solver. In Enrico Giunchiglia and Armando Tacchella, editors, Theory and Applications of Satisfiability Testing, 6th International Conference, SAT 2003. Santa Margherita Ligure, Italy, May 5\u20138, 2003 Selected Revised Papers, volume 2919 of Lecture Notes in Computer Science, pages 502\u2013518. Springer, 2003."},{"key":"11_CR11","doi-asserted-by":"crossref","unstructured":"Stephan Falke, Florian Merz, and Carsten Sinz. LLBMC: improved bounded model checking of C programs using LLVM - (competition contribution). In Nir Piterman and Scott A. Smolka, editors, Tools and Algorithms for the Construction and Analysis of Systems - 19th International Conference, TACAS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16\u201324, 2013. Proceedings, volume 7795 of Lecture Notes in Computer Science, pages 623\u2013626. Springer, 2013.","DOI":"10.1007\/978-3-642-36742-7_48"},{"key":"11_CR12","doi-asserted-by":"crossref","unstructured":"Marcelo F. Frias, Juan P. Galeotti, Carlos L\u00f3pez Pombo, and Nazareno Aguirre. Dynalloy: upgrading alloy with actions. In Gruia-Catalin Roman, William G. Griswold, and Bashar Nuseibeh, editors, 27th International Conference on Software Engineering (ICSE 2005), 15\u201321 May 2005, St. Louis, Missouri, USA, pages 442\u2013451. ACM, 2005.","DOI":"10.1145\/1062455.1062535"},{"key":"11_CR13","unstructured":"Juan P. Galeotti, Nicol\u00e1s Rosner, Carlos Gustavo L\u00f3pez Pombo, and Marcelo F. Frias. TACO: efficient sat-based bounded verification using symmetry breaking and tight bounds. IEEE Trans. Software Eng., 39(9):1283\u20131307, 2013."},{"key":"11_CR14","unstructured":"Juan P. Galeotti, Nicol\u00e1s Rosner, Carlos L\u00f3pez Pombo, and Marcelo F. Frias. Analysis of invariants for efficient bounded verification. In Paolo Tonella and Alessandro Orso, editors, Proceedings of the Nineteenth International Symposium on Software Testing and Analysis, ISSTA 2010, Trento, Italy, July 12\u201316, 2010, pages 25\u201336. ACM, 2010."},{"key":"11_CR15","unstructured":"Jaco Geldenhuys, Nazareno Aguirre, Marcelo F. Frias, and Willem Visser. Bounded lazy initialization. In Guillaume Brat, Neha Rungta, and Arnaud Venet, editors, NASA Formal Methods, 5th International Symposium, NFM 2013, Moffett Field, CA, USA, May 14\u201316, 2013. Proceedings, volume 7871 of Lecture Notes in Computer Science, pages 229\u2013243. Springer, 2013."},{"key":"11_CR16","doi-asserted-by":"crossref","unstructured":"John N. Hooker. Solving the incremental satisfiability problem. J. Log. Program., 15(1&2):177\u2013186, 1993.","DOI":"10.1016\/0743-1066(93)90018-C"},{"key":"11_CR17","unstructured":"Daniel Jackson. Software Abstractions - Logic, Language, and Analysis. MIT Press, 2006."},{"key":"11_CR18","doi-asserted-by":"crossref","unstructured":"Daniel Jackson and Mandana Vaziri. Finding bugs with a constraint solver. In Debra J. Richardson and Mary Jean Harold, editors, Proceedings of the International Symposium on Software Testing and Analysis, ISSTA 2000, Portland, OR, USA, August 21\u201324, 2000, pages 14\u201325. ACM, 2000.","DOI":"10.1145\/347324.383378"},{"key":"11_CR19","unstructured":"Sarfraz Khurshid, Corina S. Pasareanu, and Willem Visser. Generalized symbolic execution for model checking and testing. In Hubert Garavel and John Hatcliff, editors, Tools and Algorithms for the Construction and Analysis of Systems, 9th International Conference, TACAS 2003, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2003, Warsaw, Poland, April 7\u201311, 2003, Proceedings, volume 2619 of Lecture Notes in Computer Science, pages 553\u2013568. Springer, 2003."},{"key":"11_CR20","unstructured":"Daniel Kroening and Michael Tautschnig. CBMC - C bounded model checker - (competition contribution). In Erika \u00c1brah\u00e1m and Klaus Havelund, editors, Tools and Algorithms for the Construction and Analysis of Systems - 20th International Conference, TACAS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5\u201313, 2014. Proceedings, volume 8413 of Lecture Notes in Computer Science, pages 389\u2013391. Springer, 2014."},{"key":"11_CR21","unstructured":"Huu Hai Nguyen, Cristina David, Shengchao Qin, and Wei-Ngan Chin. Automated verification of shape and size properties via separation logic. In Byron Cook and Andreas Podelski, editors, Verification, Model Checking, and Abstract Interpretation, 8th International Conference, VMCAI 2007, Nice, France, January 14\u201316, 2007, Proceedings, volume 4349 of Lecture Notes in Computer Science, pages 251\u2013266. Springer, 2007."},{"key":"11_CR22","unstructured":"Aditya V. Nori, Sriram K. Rajamani, SaiDeep Tetali, and Aditya V. Thakur. The yogiproject: Software property checking via static analysis and testing. In Stefan Kowalewski and Anna Philippou, editors, Tools and Algorithms for the Construction and Analysis of Systems, 15th International Conference, TACAS 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22\u201329, 2009. Proceedings, volume 5505 of Lecture Notes in Computer Science, pages 178\u2013181. Springer, 2009."},{"key":"11_CR23","unstructured":"Corina S. Pasareanu, Willem Visser, David H. Bushnell, Jaco Geldenhuys, Peter C. Mehlitz, and Neha Rungta. Symbolic pathfinder: integrating symbolic execution with model checking for java bytecode analysis. Autom. Softw. Eng., 20(3):391\u2013425, 2013."},{"key":"11_CR24","doi-asserted-by":"crossref","unstructured":"Pablo Ponzio, Nazareno Aguirre, Marcelo F. Frias, and Willem Visser. Field-exhaustive testing. In Thomas Zimmermann, Jane Cleland-Huang, and Zhendong Su, editors, Proceedings of the 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering, FSE 2016, Seattle, WA, USA, November 13\u201318, 2016, pages 908\u2013919. ACM, 2016.","DOI":"10.1145\/2950290.2950336"},{"key":"11_CR25","doi-asserted-by":"crossref","unstructured":"Pablo Ponzio, Nicol\u00e1s Rosner, Nazareno Aguirre, and Marcelo F. Frias. Efficient tight field bounds computation based on shape predicates. In Cliff B. Jones, Pekka Pihlajasaari, and Jun Sun, editors, FM 2014: Formal Methods - 19th International Symposium, Singapore, May 12\u201316, 2014. Proceedings, volume 8442 of Lecture Notes in Computer Science, pages 531\u2013546. Springer, 2014.","DOI":"10.1007\/978-3-319-06410-9_36"},{"key":"11_CR26","unstructured":"Nicol\u00e1s Rosner, Jaco Geldenhuys, Nazareno Aguirre, Willem Visser, and Marcelo F. Frias. BLISS: improved symbolic execution by bounded lazy initialization with SAT support. IEEE Trans. Software Eng., 41(7):639\u2013660, 2015."},{"key":"11_CR27","doi-asserted-by":"crossref","unstructured":"Willem Visser and Peter C. Mehlitz. Model checking programs with java pathfinder. In Patrice Godefroid, editor, Model Checking Software, 12th International SPIN Workshop, San Francisco, CA, USA, August 22\u201324, 2005, Proceedings, volume 3639 of Lecture Notes in Computer Science, page 27. Springer, 2005.","DOI":"10.1007\/11537328_5"},{"key":"11_CR28","doi-asserted-by":"crossref","unstructured":"Willem Visser, Corina S. Pasareanu, and Radek Pel\u00e1nek. Test input generation for java containers using state matching. In Lori L. Pollock and Mauro Pezz\u00e8, editors, Proceedings of the ACM\/SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2006, Portland, Maine, USA, July 17\u201320, 2006, pages 37\u201348. ACM, 2006.","DOI":"10.1145\/1146238.1146243"}],"container-title":["Lecture Notes in Computer Science","Fundamental Approaches to Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-71500-7_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,10,23]],"date-time":"2023-10-23T09:43:55Z","timestamp":1698054235000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-71500-7_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030714994","9783030715007"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-71500-7_11","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":"20 March 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FASE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Fundamental Approaches to Software Engineering","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg City","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","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":"27 March 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1 April 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fase2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2021\/fase","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-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":"52","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":"16","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":"31% - 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":"5,5","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 changed to an online format 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)"}}]}}