{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,16]],"date-time":"2025-10-16T03:47:52Z","timestamp":1760586472456},"reference-count":31,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2008,12,11]],"date-time":"2008-12-11T00:00:00Z","timestamp":1228953600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2009,2]]},"DOI":"10.1007\/s10009-008-0090-1","type":"journal-article","created":{"date-parts":[[2008,12,11]],"date-time":"2008-12-11T08:10:44Z","timestamp":1228983044000},"page":"53-67","source":"Crossref","is-referenced-by-count":45,"title":["Symbolic execution with abstraction"],"prefix":"10.1007","volume":"11","author":[{"given":"Saswat","family":"Anand","sequence":"first","affiliation":[]},{"given":"Corina S.","family":"P\u0103s\u0103reanu","sequence":"additional","affiliation":[]},{"given":"Willem","family":"Visser","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2008,12,11]]},"reference":[{"key":"90_CR1","doi-asserted-by":"crossref","unstructured":"Anand, S., Orso, A., Harrold, M.J.: Type-dependence analysis and program transformation for symbolic execution. In: Proceedings of TACAS, pp. 117\u2013133 (2007)","DOI":"10.1007\/978-3-540-71209-1_11"},{"key":"90_CR2","doi-asserted-by":"crossref","unstructured":"Anand, S., Pasareanu, C.S., Visser, W.: Symbolic execution with abstract subsumption checking. In: Proceedings of SPIN, pp. 163\u2013181 (2006)","DOI":"10.1007\/11691617_10"},{"key":"90_CR3","doi-asserted-by":"crossref","unstructured":"Anand, S., Pasareanu, C.S., Visser, W.: JPF-SE: a symbolic execution extension to Java Pathfinder. In: Proceedings of TACAS, pp. 134\u2013138 (2007)","DOI":"10.1007\/978-3-540-71209-1_12"},{"key":"90_CR4","unstructured":"Ball, T.: A theory of predicate-complete test coverage and generation. MSR-TR-2004-28 (2004)"},{"key":"90_CR5","doi-asserted-by":"crossref","unstructured":"Ball, T., Kupferman, O., Yorsh, G.: Abstraction for falsification. In: Proceedings of CAV, pp. 67\u201381 (2005)","DOI":"10.1007\/11513988_8"},{"key":"90_CR6","doi-asserted-by":"crossref","unstructured":"Ball, T., Rajamani, S.K.: The SLAM toolkit. In: Proceedings of CAV, pp. 260\u2013264 (2001)","DOI":"10.1007\/3-540-44585-4_25"},{"issue":"6","key":"90_CR7","first-page":"388","volume":"30","author":"S. Chaki","year":"2004","unstructured":"Chaki S., Clarke E., Groce A., Jha S., Veith H.: Modular verification of software components in C. ACM Trans. Comput. Syst. 30(6), 388\u2013402 (2004)","journal-title":"ACM Trans. Comput. Syst."},{"key":"90_CR8","doi-asserted-by":"crossref","unstructured":"Dams, D., Namjoshi, K.S.: Shape analysis through predicate abstraction and model checking. In: Proceedings of VMCAI, pp. 310\u2013324 (2003)","DOI":"10.1007\/3-540-36384-X_25"},{"key":"90_CR9","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Qadeer, S.: Predicate abstraction for software verification. In: Proceedings of POPL, pp. 191\u2013202 (2002)","DOI":"10.1145\/503272.503291"},{"key":"90_CR10","doi-asserted-by":"crossref","unstructured":"Flyod, R.W.: Assigning meanings to programs. In: Proceedings of symposia in applied mathematics, vol. 19, pp. 19\u201332 (1967)","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"90_CR11","doi-asserted-by":"crossref","unstructured":"Ghiya, R., Hendren, L.J.: Is it a tree, a DAG, or a cyclic graph? a shape analysis for heap-directed pointers in c. In: Proceedings of POPL, pp. 1\u201315 (1996)","DOI":"10.1145\/237721.237724"},{"key":"90_CR12","doi-asserted-by":"crossref","unstructured":"Godefroid, P., Klarlund, N., Sen, K.: DART: Directed automated random testing. In: Proceedings of PLDI, pp. 213\u2013223 (2005)","DOI":"10.1145\/1065010.1065036"},{"key":"90_CR13","doi-asserted-by":"crossref","unstructured":"Gopan, D., DiMaio, F., Dor, N., Reps, T., Sagiv, M.: Numeric domains with summarized dimensions. In: Proceedings of TACAS, pp. 512\u2013529 (2004)","DOI":"10.1007\/978-3-540-24730-2_38"},{"key":"90_CR14","doi-asserted-by":"crossref","unstructured":"Gopan, D., Reps, T., Sagiv, M.: A framework for numeric analysis of array operations. In: Proceedings of POPL, pp. 338\u2013350 (2005)","DOI":"10.1145\/1040305.1040333"},{"key":"90_CR15","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Software verification with BLAST. In: Proceedings of SPIN, pp. 235\u2013239 (2003)","DOI":"10.1007\/3-540-44829-2_17"},{"key":"90_CR16","doi-asserted-by":"crossref","unstructured":"Holzmann, G.J., Joshi, R.: Model-driven software verification. In: Proceedings of SPIN, pp. 76\u201391 (2004)","DOI":"10.1007\/978-3-540-24732-6_6"},{"key":"90_CR17","unstructured":"Java PathFinder. http:\/\/javapathfinder.sourceforge.net"},{"key":"90_CR18","doi-asserted-by":"crossref","unstructured":"Khurshid, S., P\u0103s\u0103reanu, C., Visser, W.: Generalized symbolic execution for model checking and testing. In: Proceedings of TACAS, pp. 553\u2013568 (2003)","DOI":"10.1007\/3-540-36577-X_40"},{"key":"90_CR19","doi-asserted-by":"crossref","unstructured":"Khurshid, S., Suen, Y.: Generalizing symbolic execution to library classes. In: Proceedings of PASTE, pp. 103\u2013110 (2005)","DOI":"10.1145\/1108792.1108817"},{"issue":"7","key":"90_CR20","doi-asserted-by":"crossref","first-page":"385","DOI":"10.1145\/360248.360252","volume":"19","author":"J.C. King","year":"1976","unstructured":"King J.C.: Symbolic execution and program testing. Commun. ACM 19(7), 385\u2013394 (1976)","journal-title":"Commun. ACM"},{"key":"90_CR21","doi-asserted-by":"crossref","unstructured":"Kuncak, V., Rinard, M.: Existential heap abstraction entailment is undecidable. In: Proceedings of SAS, pp. 418\u2013438 (2003)","DOI":"10.1007\/3-540-44898-5_24"},{"key":"90_CR22","doi-asserted-by":"crossref","unstructured":"Manevich, R., Yahav, E., Ramalingam, G., Sagiv, M.: Predicate abstraction and canonical abstraction for singly-linked lists. In: Proceedings of VMCAI, pp. 181\u2013198 (2005)","DOI":"10.1007\/978-3-540-30579-8_13"},{"key":"90_CR23","doi-asserted-by":"crossref","unstructured":"P\u0103s\u0103reanu, C., Visser, W.: Verification of Java programs using symbolic execution and invariant generation. In: Proceedings of SPIN, pp. 164\u2013181 (2004)","DOI":"10.1007\/978-3-540-24732-6_13"},{"issue":"1","key":"90_CR24","doi-asserted-by":"crossref","first-page":"34","DOI":"10.1007\/s10009-002-0088-z","volume":"5","author":"C.S. P\u0103s\u0103reanu","year":"2003","unstructured":"P\u0103s\u0103reanu C.S., Dwyer M.B., Visser W.: Finding feasible abstract counter-examples. STTT 5(1), 34\u201348 (2003)","journal-title":"STTT"},{"key":"90_CR25","doi-asserted-by":"crossref","unstructured":"P\u0103s\u0103reanu, C.S., Pel\u00e1nek, R., Visser, W.: Concrete model checking with abstract matching and refinement. In: Proceedings of CAV, pp. 52\u201366 (2005)","DOI":"10.1007\/11513988_7"},{"key":"90_CR26","doi-asserted-by":"crossref","unstructured":"Pugh, W.: The Omega test: a fast and practical integer programming algorithm for dependence analysis. Commun. ACM, 31(8), August (1992)","DOI":"10.1145\/135226.135233"},{"issue":"3","key":"90_CR27","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1145\/514188.514190","volume":"24","author":"S. Sagiv","year":"2002","unstructured":"Sagiv S., Reps T.W., Wilhelm R.: Parametric shape analysis via 3-valued logic. ACM Trans. Program. Lang. Syst. 24(3), 217\u2013298 (2002)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"90_CR28","doi-asserted-by":"crossref","unstructured":"Sen, K., Marinov, D., Agha, G.: CUTE: a concolic unit testing engine for C. In: Proceedings of ESEC\/SIGSOFT FSE, pp. 263\u2013272 (2005)","DOI":"10.1145\/1081706.1081750"},{"issue":"2","key":"90_CR29","doi-asserted-by":"crossref","first-page":"203","DOI":"10.1023\/A:1022920129859","volume":"10","author":"W. Visser","year":"2003","unstructured":"Visser W., Havelund K., Brat G., Park S.J., Lerda F.: Model checking programs. Autom Softw Eng J 10(2), 203\u2013232 (2003)","journal-title":"Autom Softw Eng J"},{"key":"90_CR30","doi-asserted-by":"crossref","unstructured":"Xie, T., Marinov, D., Schulte, W., Notkin, D.: Symstra: a framework for generating object-oriented unit tests using symbolic execution. In: Proceedings of TACAS, pp. 365\u2013381 (2005)","DOI":"10.1007\/978-3-540-31980-1_24"},{"key":"90_CR31","doi-asserted-by":"crossref","unstructured":"Yavuz-Kahveci, T., Bultan, T.: Automated verification of concurrent linked lists with counters. In: Proceedings of SAS, pp. 69\u201384 (2002)","DOI":"10.1007\/3-540-45789-5_8"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-008-0090-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-008-0090-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-008-0090-1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,29]],"date-time":"2019-05-29T03:25:24Z","timestamp":1559100324000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-008-0090-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,12,11]]},"references-count":31,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2009,2]]}},"alternative-id":["90"],"URL":"https:\/\/doi.org\/10.1007\/s10009-008-0090-1","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008,12,11]]}}}