{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T05:53:13Z","timestamp":1743141193878,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":36,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662491218"},{"type":"electronic","value":"9783662491225"}],"license":[{"start":{"date-parts":[[2015,12,25]],"date-time":"2015-12-25T00:00:00Z","timestamp":1451001600000},"content-version":"unspecified","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":[[2016]]},"DOI":"10.1007\/978-3-662-49122-5_10","type":"book-chapter","created":{"date-parts":[[2015,12,24]],"date-time":"2015-12-24T05:01:36Z","timestamp":1450933296000},"page":"206-225","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Exact Heap Summaries for Symbolic Execution"],"prefix":"10.1007","author":[{"given":"Benjamin","family":"Hillery","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Eric","family":"Mercer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Neha","family":"Rungta","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Suzette","family":"Person","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,12,25]]},"reference":[{"key":"10_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/978-3-540-30538-5_9","volume-title":"FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science","author":"J Berdine","year":"2004","unstructured":"Berdine, J., Calcagno, C., O\u2019hearn, P.W.: A decidable fragment of separation logic. In: Lodaya, K., Mahajan, M. (eds.) FSTTCS 2004. LNCS, vol. 3328, pp. 97\u2013109. Springer, Heidelberg (2004)"},{"key":"10_CR2","doi-asserted-by":"crossref","unstructured":"Blackshear, S., Chang, B.Y.E., Sridharan, M.: Thresher: Precise refutations for heap reachability. In: Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation PLDI 2013, pp. 275\u2013286. ACM, New York (2013)","DOI":"10.1145\/2491956.2462186"},{"key":"10_CR3","doi-asserted-by":"crossref","unstructured":"Boyapati, C., Khurshid, S., Marinov, D.: Korat: automated testing based on java predicates. In: ACM SIGSOFT Software Engineering Notes, vol. 27, pp. 123\u2013133. ACM (2002)","DOI":"10.1145\/566171.566191"},{"key":"10_CR4","doi-asserted-by":"crossref","unstructured":"Braione, P., Denaro, G., Pezz\u00e8, M.: Symbolic execution of programs with heap inputs. In: Proceedings of the 2015 10th Joint Meeting on Foundations of Software Engineering, pp. 602\u2013613. ACM (2015)","DOI":"10.1145\/2786805.2786842"},{"key":"10_CR5","doi-asserted-by":"crossref","unstructured":"Brotherston, J., Fuhs, C., P\u00e9rez, J.A.N., Gorogiannis, N.: A decision procedure for satisfiability in separation logic with inductive predicates. In: Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS), p. 25. ACM (2014)","DOI":"10.1145\/2603088.2603091"},{"key":"10_CR6","unstructured":"Cadar, C., Dunbar, D., Engler, D.R.: Klee: Unassisted and automatic generation of high-coverage tests for complex systems programs. In: Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation OSDI 2008, pp. 209\u2013224. USENIX Association, Berkeley (2008)"},{"issue":"7","key":"10_CR7","doi-asserted-by":"publisher","first-page":"1758","DOI":"10.1016\/j.future.2012.02.006","volume":"29","author":"T Chen","year":"2013","unstructured":"Chen, T., Zhang, X.S., Guo, S.Z., Li, H.Y., Wu, Y.: State of the art: Dynamic symbolic execution for automated test generation. Future Gener. Comput. Syst. 29(7), 1758\u20131773 (2013)","journal-title":"Future Gener. Comput. Syst."},{"key":"10_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1007\/978-3-642-23217-6_16","volume-title":"CONCUR 2011 \u2013 Concurrency Theory","author":"B Cook","year":"2011","unstructured":"Cook, B., Haase, C., Ouaknine, J., Parkinson, M., Worrell, J.: Tractable reasoning in a fragment of separation logic. In: Katoen, J.-P., K\u00f6nig, B. (eds.) CONCUR 2011. LNCS, vol. 6901, pp. 235\u2013249. Springer, Heidelberg (2011)"},{"key":"10_CR9","doi-asserted-by":"crossref","unstructured":"Deng, X., Lee, J., et al.: Bogor\/kiasan: A k-bounded symbolic execution for checking strong heap properties of open systems. In: 21st IEEE\/ACM International Conference on Automated Software Engineering ASE 2006, pp. 157\u2013166. IEEE (2006)","DOI":"10.1109\/ASE.2006.26"},{"key":"10_CR10","doi-asserted-by":"crossref","unstructured":"Deng, X., Robby, Hatcliff, J.: Kiasan\/KUnit: Automatic test case generation and analysis feedback for open object-oriented systems. In: TAICPART-MUTATION, pp. 3\u201312 (2007)","DOI":"10.1109\/TAIC.PART.2007.32"},{"key":"10_CR11","doi-asserted-by":"crossref","unstructured":"Deng, X., Robby, Hatcliff, J.: Towards a case-optimal symbolic execution algorithm for analyzing strong properties of object-oriented programs. In: Fifth IEEE International Conference on Software Engineering and Formal Methods SEFM 2007, pp. 273\u2013282, September 2007","DOI":"10.1109\/SEFM.2007.43"},{"key":"10_CR12","doi-asserted-by":"crossref","unstructured":"Dillig, I., Dillig, T., Aiken, A., Sagiv, M.: Precise and compact modular procedure summaries for heap manipulating programs. In: Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation PLDI 2011, pp. 567\u2013577. ACM, New York (2011)","DOI":"10.1145\/1993498.1993565"},{"issue":"1","key":"10_CR13","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/2693208.2693248","volume":"40","author":"Marko Dimja\u0161evi\u0107","year":"2015","unstructured":"Dimja\u0161evi\u0107, M., Giannakopoulou, D., Howar, F., Isberner, M., Rakamari\u0107, Z., Raman, V.: The dart, the psyco, and the doop. In: ACM SIGSOFT Software Engineering Notes, vol. 40, pp. 1\u20135. ACM (2015)","journal-title":"ACM SIGSOFT Software Engineering Notes"},{"key":"10_CR14","doi-asserted-by":"crossref","unstructured":"Elkarablieh, B., Godefroid, P., Levin, M.Y.: Precise pointer reasoning for dynamic test generation. In: Proceedings of the Eighteenth International Symposium on Software Testing and Analysis, pp. 129\u2013140. ACM (2009)","DOI":"10.1145\/1572272.1572288"},{"issue":"2","key":"10_CR15","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1016\/0304-3975(92)90014-7","volume":"103","author":"M Felleisen","year":"1992","unstructured":"Felleisen, M., Hieb, R.: The revised report on the syntactic theories of sequential control and state. Theoret. Comput. Sci. 103(2), 235\u2013271 (1992)","journal-title":"Theoret. Comput. Sci."},{"key":"10_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"393","DOI":"10.1007\/978-3-662-46081-8_22","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"P Ferrara","year":"2015","unstructured":"Ferrara, P., M\u00fcller, P., Novacek, M.: Automatic inference of heap properties exploiting value domains. In: D\u2019Souza, D., Lal, A., Larsen, K.G. (eds.) VMCAI 2015. LNCS, vol. 8931, pp. 393\u2013411. Springer, Heidelberg (2015)"},{"key":"10_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"222","DOI":"10.1007\/978-3-319-23404-5_15","volume-title":"Model Checking Software","author":"A Filieri","year":"2015","unstructured":"Filieri, A., Frias, M.F., P\u0103s\u0103reanu, C.S., Visser, W.: Model counting for complex data structures. In: Fischer, B., Geldenhuys, J. (eds.) SPIN 2015. LNCS, vol. 9232, pp. 222\u2013241. Springer, Heidelberg (2015)"},{"key":"10_CR18","doi-asserted-by":"crossref","unstructured":"Giannakopoulou, D., Howar, F., Isberner, M., Lauderdale, T., Rakamari\u0107, Z., Raman, V.: Taming test inputs for separation assurance. In: Proceedings of the 29th IEEE\/ACM International Conference on Automated Software Engineering (ASE), pp. 373\u2013384. ACM (2014)","DOI":"10.1145\/2642937.2642940"},{"issue":"1","key":"10_CR19","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2557833.2560579","volume":"39","author":"B Hillery","year":"2014","unstructured":"Hillery, B., Mercer, E., Rungta, N., Person, S.: Towards a lazier symbolic pathfinder. SIGSOFT Softw. Eng. Notes 39(1), 1\u20135 (2014)","journal-title":"SIGSOFT Softw. Eng. Notes"},{"key":"10_CR20","unstructured":"Hillery, B., Mercer, E., Rungta, N., Person, S.: Exact heap summaries for symbolic execution. Technical report, Brigham Young University (2015). http:\/\/students.cs.byu.edu\/egm\/papers\/SH-long.pdf"},{"key":"10_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)"},{"key":"10_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.S.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"10_CR23","doi-asserted-by":"crossref","unstructured":"Navarro P\u00e9rez, J.A., Rybalchenko, A.: Separation logic+ superposition calculus = heap theorem prover. In: ACM SIGPLAN Notices, vol. 46, pp. 556\u2013566. ACM (2011)","DOI":"10.1145\/1993316.1993563"},{"key":"10_CR24","doi-asserted-by":"crossref","unstructured":"Person, S., Yang, G., Rungta, N., Khurshid, S.: Directed incremental symbolic execution. In: PLDI, pp. 504\u2013515 (2011)","DOI":"10.1145\/1993316.1993558"},{"key":"10_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"711","DOI":"10.1007\/978-3-319-08867-9_47","volume-title":"Computer Aided Verification","author":"R Piskac","year":"2014","unstructured":"Piskac, R., Wies, T., Zufferey, D.: Automating separation logic with trees and data. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 711\u2013728. Springer, Heidelberg (2014)"},{"issue":"3","key":"10_CR26","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.H., Geldenhuys, J., Mehlitz, P.C., Rungta, N.: Symbolic PathFinder: integrating symbolic execution with model checking for Java bytecode analysis. Autom. Softw. Eng. 20(3), 391\u2013425 (2013)","journal-title":"Autom. Softw. Eng."},{"key":"10_CR27","doi-asserted-by":"crossref","unstructured":"Qu, X., Robinson, B.: A case study of concolic testing tools and their limitations. In: 2011 International Symposium on Empirical Software Engineering and Measurement (ESEM), pp. 117\u2013126. IEEE (2011)","DOI":"10.1109\/ESEM.2011.20"},{"key":"10_CR28","doi-asserted-by":"crossref","unstructured":"Rosner, N., Geldenhuys, J., Aguirre, N., Visser, W., Frias, M.: BLISS: Improved symbolic execution by bounded lazy initialization with sat support. Software Engineering, IEEE Transactions on PP(99), 1\u20131 (2015)","DOI":"10.1109\/TSE.2015.2389225"},{"key":"10_CR29","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511792588","volume-title":"Introduction to Bisimulation and Coinduction","author":"D Sangiorgi","year":"2011","unstructured":"Sangiorgi, D.: Introduction to Bisimulation and Coinduction. Cambridge University Press, New York (2011)"},{"key":"10_CR30","doi-asserted-by":"crossref","unstructured":"Sen, K., Necula, G., Gong, L., Choi, P.W.: MultiSE: Multi-path symbolic execution using value summaries. Technical Report UCB\/EECS-2014-173, University of California at Berkely Department of Electrical Engineering and Computer Sciences, October 2014","DOI":"10.1145\/2786805.2786830"},{"key":"10_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/978-3-540-79124-9_10","volume-title":"Tests and Proofs","author":"Nikolai Tillmann","year":"2008","unstructured":"Tillmann, Nikolai, de Halleux, Jonathan: Pex\u2013White Box Test Generation for.NET. In: Beckert, Bernhard, H\u00e4hnle, Reiner (eds.) TAP 2008. LNCS, vol. 4966, pp. 134\u2013153. Springer, Heidelberg (2008)"},{"key":"10_CR32","doi-asserted-by":"crossref","unstructured":"Torlak, E., Bodik, R.: A lightweight symbolic virtual machine for solver-aided host languages. In: Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation, p. 54. ACM (2014)","DOI":"10.1145\/2594291.2594340"},{"issue":"4","key":"10_CR33","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1145\/1013886.1007526","volume":"29","author":"W Visser","year":"2004","unstructured":"Visser, W., P\u01ces\u01cereanu, C.S., Khurshid, S.: Test input generation with Java PathFinder. ACM SIGSOFT Softw. Eng. Notes 29(4), 97\u2013107 (2004)","journal-title":"ACM SIGSOFT Softw. Eng. Notes"},{"key":"10_CR34","unstructured":"Wesonga, S.O.: Javalite - An Operational Semantics for Modeling Java Programs. Master\u2019s thesis, Brigham Young University, Provo UT (2012)"},{"key":"10_CR35","doi-asserted-by":"crossref","unstructured":"Xie, Y., Aiken, A.: Scalable error detection using boolean satisfiability. In: Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages POPL 2005, pp. 351\u2013363. ACM, New York (2005)","DOI":"10.1145\/1047659.1040334"},{"key":"10_CR36","doi-asserted-by":"crossref","unstructured":"Yorsh, G., Yahav, E., Chandra, S.: Generating precise and concise procedure summaries. In: ACM SIGPLAN Notices, vol. 43, pp. 221\u2013234. ACM (2008)","DOI":"10.1145\/1328897.1328467"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-49122-5_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,5,30]],"date-time":"2022-05-30T17:42:16Z","timestamp":1653932536000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-49122-5_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,12,25]]},"ISBN":["9783662491218","9783662491225"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-49122-5_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015,12,25]]},"assertion":[{"value":"25 December 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}