{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:42:43Z","timestamp":1780994563073,"version":"3.54.1"},"publisher-location":"Cham","reference-count":37,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030317836","type":"print"},{"value":"9783030317843","type":"electronic"}],"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-31784-3_12","type":"book-chapter","created":{"date-parts":[[2019,10,21]],"date-time":"2019-10-21T01:32:04Z","timestamp":1571621524000},"page":"209-227","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":12,"title":["Enhancing Symbolic Execution of Heap-Based Programs with Separation Logic for Test Input Generation"],"prefix":"10.1007","author":[{"given":"Long H.","family":"Pham","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Quang Loc","family":"Le","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Quoc-Sang","family":"Phan","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jun","family":"Sun","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Shengchao","family":"Qin","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2019,10,21]]},"reference":[{"key":"12_CR1","unstructured":"Facebook Infer. https:\/\/fbinfer.com\/"},{"key":"12_CR2","unstructured":"JaCoCo. https:\/\/www.eclemma.org\/jacoco\/"},{"key":"12_CR3","unstructured":"JBSE. https:\/\/github.com\/pietrobraione\/jbse"},{"key":"12_CR4","unstructured":"SIR. http:\/\/sir.unl.edu\/portal\/index.php"},{"key":"12_CR5","unstructured":"Sireum. https:\/\/code.google.com\/archive\/p\/sireum\/downloads"},{"key":"12_CR6","unstructured":"SUSHI Experiments. https:\/\/github.com\/pietrobraione\/sushi-experiments"},{"key":"12_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/11575467_5","volume-title":"Programming Languages and Systems","author":"J Berdine","year":"2005","unstructured":"Berdine, J., Calcagno, C., O\u2019Hearn, P.W.: Symbolic execution with separation logic. In: Yi, K. (ed.) APLAS 2005. LNCS, vol. 3780, pp. 52\u201368. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11575467_5"},{"key":"12_CR8","doi-asserted-by":"publisher","unstructured":"Braione, P., Denaro, G., Mattavelli, A., Pezz\u00e8, M.: Combining symbolic execution and search-based testing for programs with complex heap inputs. In: Bultan, T., Sen, K. (eds.) ISSTA 2017, pp. 90\u2013101. ACM (2017). https:\/\/doi.org\/10.1145\/3092703.3092715","DOI":"10.1145\/3092703.3092715"},{"key":"12_CR9","doi-asserted-by":"publisher","unstructured":"Braione, P., Denaro, G., Pezz\u00e8, M.: Symbolic execution of programs with heap inputs. In: Nitto, E.D., Harman, M., Heymans, P. (eds.) FSE 2015, pp. 602\u2013613. ACM (2015). https:\/\/doi.org\/10.1145\/2786805.2786842","DOI":"10.1145\/2786805.2786842"},{"key":"12_CR10","doi-asserted-by":"publisher","unstructured":"Braione, P., Denaro, G., Pezz\u00e8, M.: JBSE: a symbolic executor for Java programs with complex heap inputs. In: Zimmermann, T., Cleland-Huang, J., Su, Z. (eds.) FSE 2016, pp. 1018\u20131022. ACM (2016). https:\/\/doi.org\/10.1145\/2950290.2983940","DOI":"10.1145\/2950290.2983940"},{"key":"12_CR11","doi-asserted-by":"publisher","unstructured":"Cadar, C., et al.: Symbolic execution for software testing in practice: preliminary assessment. In: Taylor, R.N., Gall, H.C., Medvidovic, N. (eds.) ICSE 2011, pp. 1066\u20131071. ACM (2011). https:\/\/doi.org\/10.1145\/1985793.1985995","DOI":"10.1145\/1985793.1985995"},{"issue":"6","key":"12_CR12","doi-asserted-by":"publisher","first-page":"26:1","DOI":"10.1145\/2049697.2049700","volume":"58","author":"C Calcagno","year":"2011","unstructured":"Calcagno, C., Distefano, D., O\u2019Hearn, P.W., Yang, H.: Compositional shape analysis by means of bi-abduction. JACM 58(6), 26:1\u201326:66 (2011). https:\/\/doi.org\/10.1145\/2049697.2049700","journal-title":"JACM"},{"issue":"9","key":"12_CR13","doi-asserted-by":"publisher","first-page":"1006","DOI":"10.1016\/j.scico.2010.07.004","volume":"77","author":"WN Chin","year":"2012","unstructured":"Chin, W.N., David, C., Nguyen, H.H., Qin, S.: Automated verification of shape, size and bag properties via user-defined predicates in separation logic. Sci. Comput. Program. 77(9), 1006\u20131036 (2012). https:\/\/doi.org\/10.1016\/j.scico.2010.07.004","journal-title":"Sci. Comput. Program."},{"key":"12_CR14","doi-asserted-by":"publisher","unstructured":"Deng, X., Lee, J., Robby: Bogor\/Kiasan: a K-bounded symbolic execution for checking strong heap properties of open systems. In: ASE 2006, pp. 157\u2013166. IEEE Computer Society (2006). https:\/\/doi.org\/10.1109\/ASE.2006.26","DOI":"10.1109\/ASE.2006.26"},{"key":"12_CR15","doi-asserted-by":"publisher","unstructured":"Deng, X., Robby, Hatcliff, J.: Towards a case-optimal symbolic execution algorithm for analyzing strong properties of object-oriented programs. In: SEFM 2007. IEEE Computer Society (2007). https:\/\/doi.org\/10.1109\/SEFM.2007.43","DOI":"10.1109\/SEFM.2007.43"},{"key":"12_CR16","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1016\/B978-0-08-049646-7.50008-4","volume-title":"A Mathematical Introduction to Logic","author":"Herbert B. Enderton","year":"2001","unstructured":"Enderton, H.B.: A Mathematical Introduction to Logic, 2nd Edn. pp. 67\u2013181. Academic Press (2001). https:\/\/doi.org\/10.1016\/B978-0-08-049646-7.50008-4"},{"key":"12_CR17","doi-asserted-by":"publisher","unstructured":"Galeotti, J.P., Rosner, N., L\u00f3pez Pombo, C.G., Frias, M.F.: Analysis of invariants for efficient bounded verification. In: Tonella, P., Orso, A. (eds.) ISSTA 2010, pp. 25\u201336. ACM (2010). https:\/\/doi.org\/10.1145\/1831708.1831712","DOI":"10.1145\/1831708.1831712"},{"key":"12_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1007\/978-3-642-38088-4_16","volume-title":"NASA Formal Methods","author":"J Geldenhuys","year":"2013","unstructured":"Geldenhuys, J., Aguirre, N., Frias, M.F., Visser, W.: Bounded lazy initialization. In: Brat, G., Rungta, N., Venet, A. (eds.) NFM 2013. LNCS, vol. 7871, pp. 229\u2013243. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-38088-4_16"},{"key":"12_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"206","DOI":"10.1007\/978-3-662-49122-5_10","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"B Hillery","year":"2016","unstructured":"Hillery, B., Mercer, E., Rungta, N., Person, S.: Exact heap summaries for symbolic execution. In: Jobstmann, B., Leino, K.R.M. (eds.) VMCAI 2016. LNCS, vol. 9583, pp. 206\u2013225. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49122-5_10"},{"key":"12_CR20","doi-asserted-by":"publisher","unstructured":"Ishtiaq, S.S., O\u2019Hearn, P.W.: BI as an assertion language for mutable data structures. In: Hankin, C., Schmidt, D. (eds.) POPL 2001, pp. 14\u201326. ACM (2001). https:\/\/doi.org\/10.1145\/360204.375719","DOI":"10.1145\/360204.375719"},{"key":"12_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"553","DOI":"10.1007\/3-540-36577-X_40","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Khurshid","year":"2003","unstructured":"Khurshid, S., P\u0103s\u0103reanu, C.S., Visser, W.: Generalized symbolic execution for model checking and testing. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 553\u2013568. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/3-540-36577-X_40"},{"issue":"7","key":"12_CR22","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1145\/360248.360252","volume":"19","author":"JC King","year":"1976","unstructured":"King, J.C.: Symbolic execution and program testing. Commun. ACM 19(7), 385\u2013394 (1976). https:\/\/doi.org\/10.1145\/360248.360252","journal-title":"Commun. ACM"},{"key":"12_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/978-3-319-08867-9_4","volume-title":"Computer Aided Verification","author":"QL Le","year":"2014","unstructured":"Le, Q.L., Gherghina, C., Qin, S., Chin, W.-N.: Shape analysis via second-order bi-abduction. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 52\u201368. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_4"},{"key":"12_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"382","DOI":"10.1007\/978-3-319-41528-4_21","volume-title":"Computer Aided Verification","author":"QL Le","year":"2016","unstructured":"Le, Q.L., Sun, J., Chin, W.-N.: Satisfiability modulo heap-based programs. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 382\u2013404. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41528-4_21"},{"key":"12_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/978-3-319-89960-2_3","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"QL Le","year":"2018","unstructured":"Le, Q.L., Sun, J., Qin, S.: Frame inference for inductive entailment proofs in separation logic. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10805, pp. 41\u201360. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89960-2_3"},{"key":"12_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"495","DOI":"10.1007\/978-3-319-63390-9_26","volume-title":"Computer Aided Verification","author":"QL Le","year":"2017","unstructured":"Le, Q.L., Tatsuta, M., Sun, J., Chin, W.-N.: A decidable fragment in separation logic with inductive predicates and arithmetic. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 495\u2013517. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63390-9_26"},{"key":"12_CR27","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/978-1-4615-5229-1_12","volume-title":"Behavioral Specifications of Businesses and Systems","author":"GT Leavens","year":"1999","unstructured":"Leavens, G.T., Baker, A.L., Ruby, C.: JML: a notation for detailed design. In: Kilov, H., Rumpe, B., Simmonds, I. (eds.) Behavioral Specifications of Businesses and Systems, vol. 523, pp. 175\u2013188. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/978-1-4615-5229-1_12"},{"key":"12_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"405","DOI":"10.1007\/978-3-319-41528-4_22","volume-title":"Computer Aided Verification","author":"P M\u00fcller","year":"2016","unstructured":"M\u00fcller, P., Schwerhoff, M., Summers, A.J.: Automatic verification of iterated separating conjunctions using symbolic execution. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 405\u2013425. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41528-4_22"},{"key":"12_CR29","first-page":"442","volume-title":"Lecture Notes in Computer Science","author":"Long H. Pham","year":"2019","unstructured":"Pham, L.H., Le, Q.L., Phan, Q.S., Sun, J.: Concolic testing heap-manipulating programs. In: FM 2019 (2019, to appear)"},{"key":"12_CR30","doi-asserted-by":"publisher","unstructured":"Pham, L.H., Le, Q.L., Phan, Q.S., Sun, J., Qin, S.: Testing heap-based programs with Java StarFinder. In: Chaudron, M., Crnkovic, I., Chechik, M., Harman, M. (eds.) ICSE 2018, pp. 268\u2013269. ACM (2018). https:\/\/doi.org\/10.1145\/3183440.3194964","DOI":"10.1145\/3183440.3194964"},{"issue":"3","key":"12_CR31","doi-asserted-by":"publisher","first-page":"391","DOI":"10.1007\/s10515-013-0122-2","volume":"20","author":"CS P\u0103s\u0103reanu","year":"2013","unstructured":"P\u0103s\u0103reanu, C.S., Visser, W., Bushnell, D., Geldenhuys, J., Mehlitz, P., Rungta, N.: Symbolic PathFinder: integrating symbolic execution with model checking for Java bytecode analysis. Autom. Softw. Eng. 20(3), 391\u2013425 (2013). https:\/\/doi.org\/10.1007\/s10515-013-0122-2","journal-title":"Autom. Softw. Eng."},{"key":"12_CR32","doi-asserted-by":"publisher","unstructured":"Reynolds, J.: Separation logic: a logic for shared mutable data structures. In: LICS 2002, pp. 55\u201374. IEEE Computer Society (2002). https:\/\/doi.org\/10.1109\/LICS.2002.1029817","DOI":"10.1109\/LICS.2002.1029817"},{"issue":"7","key":"12_CR33","doi-asserted-by":"publisher","first-page":"639","DOI":"10.1109\/TSE.2015.2389225","volume":"41","author":"N Rosner","year":"2015","unstructured":"Rosner, N., Geldenhuys, J., Aguirre, N., Visser, W., Frias, M.F.: BLISS: improved symbolic execution by bounded lazy initialization with SAT support. IEEE Trans. Softw. Eng. 41(7), 639\u2013660 (2015). https:\/\/doi.org\/10.1109\/TSE.2015.2389225","journal-title":"IEEE Trans. Softw. Eng."},{"key":"12_CR34","doi-asserted-by":"publisher","unstructured":"Schwartz, E.J., Avgerinos, T., Brumley, D.: All you ever wanted to know about dynamic taint analysis and forward symbolic execution (but Might Have Been Afraid to Ask). In: S&P 2010, pp. 317\u2013331. IEEE Computer Society (2010). https:\/\/doi.org\/10.1109\/SP.2010.26","DOI":"10.1109\/SP.2010.26"},{"key":"12_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1007\/978-3-319-47958-3_22","volume-title":"Programming Languages and Systems","author":"M Tatsuta","year":"2016","unstructured":"Tatsuta, M., Le, Q.L., Chin, W.-N.: Decision procedure for separation logic with inductive definitions and presburger arithmetic. In: Igarashi, A. (ed.) APLAS 2016. LNCS, vol. 10017, pp. 423\u2013443. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-47958-3_22"},{"key":"12_CR36","doi-asserted-by":"publisher","unstructured":"Visser, W., P\u01ces\u01cereanu, C.S., Khurshid, S.: Test input generation with Java PathFinder. In: Avrunin, G.S., Rothermel, G. (eds.) ISSTA 2004, pp. 97\u2013107. ACM (2004). https:\/\/doi.org\/10.1145\/1007512.1007526","DOI":"10.1145\/1007512.1007526"},{"key":"12_CR37","doi-asserted-by":"crossref","unstructured":"Zheng, G., Le, Q.L., Nguyen, T., Phan, Q.S.: Automatic data structure repair using separation logic. In: JPF 2018 (2018)","DOI":"10.1145\/3282517.3282528"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-31784-3_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,7,25]],"date-time":"2024-07-25T08:37:50Z","timestamp":1721896670000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-31784-3_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030317836","9783030317843"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-31784-3_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"21 October 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ATVA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Automated Technology for Verification and Analysis","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Taipei","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Taiwan","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":"28 October 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31 October 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"atva2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/atva2019.iis.sinica.edu.tw\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Open","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":"87","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":"29","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":"33% - 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.4","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":"Between 1 and 2","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)"}}]}}