{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,31]],"date-time":"2025-05-31T23:10:02Z","timestamp":1748733002451,"version":"3.41.0"},"publisher-location":"Berlin, Heidelberg","reference-count":37,"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_16","type":"book-chapter","created":{"date-parts":[[2015,12,24]],"date-time":"2015-12-24T05:01:36Z","timestamp":1450933296000},"page":"328-347","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":23,"title":["Abstraction-driven Concolic Testing"],"prefix":"10.1007","author":[{"given":"Przemys\u0142aw","family":"Daca","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ashutosh","family":"Gupta","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas A.","family":"Henzinger","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,12,25]]},"reference":[{"key":"16_CR1","unstructured":"CRABS tool. http:\/\/pub.ist.ac.at\/~przemek\/crabs_tool.html"},{"key":"16_CR2","unstructured":"Radio Technical Commission for Aeronautics. www.rtca.org"},{"issue":"1","key":"16_CR3","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/565816.503274","volume":"37","author":"Thomas Ball","year":"2002","unstructured":"Ball, T., Rajamani, S.K.: The SLAM project: debugging system software via static analysis. In: POPL (2002)","journal-title":"ACM SIGPLAN Notices"},{"key":"16_CR4","doi-asserted-by":"crossref","unstructured":"Banerjee, A., Chattopadhyay, S., Roychoudhury, A.: Static analysis driven cache performance testing. In: RTSS, pp. 319\u2013329 (2013)","DOI":"10.1109\/RTSS.2013.39"},{"key":"16_CR5","doi-asserted-by":"crossref","unstructured":"Beckman, N.E., Nori, A.V., Rajamani, S.K., Simmons, R.J.: Proofs from tests. In: ISSTA, pp. 3\u201314 (2008)","DOI":"10.1145\/1390630.1390634"},{"key":"16_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"401","DOI":"10.1007\/978-3-662-46681-0_31","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Beyer","year":"2015","unstructured":"Beyer, D.: Software verification and verifiable witnesses. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 401\u2013416. Springer, Heidelberg (2015). (Report on SV-COMP 2015)"},{"key":"16_CR7","doi-asserted-by":"crossref","unstructured":"Beyer, D., Chlipala, A., Henzinger, T.A., Jhala, R., Majumdar, R.: Generating tests from counterexamples. In: Finkelstein, A., Estublier, J., Rosenblum, D.S. (eds.) ICSE, pp. 326\u2013335. IEEE Computer Society (2004)","DOI":"10.1109\/ICSE.2004.1317455"},{"key":"16_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1007\/978-3-642-22110-1_16","volume-title":"Computer Aided Verification","author":"D Beyer","year":"2011","unstructured":"Beyer, D., Keremoglu, M.E.: CPAchecker: A tool for configurable software verification. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 184\u2013190. Springer, Heidelberg (2011)"},{"issue":"3","key":"16_CR9","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1147\/sj.223.0229","volume":"22","author":"DL Bird","year":"1983","unstructured":"Bird, D.L., Munoz, C.U.: Automatic generation of random self-checking test cases. IBM Syst. J. 22(3), 229\u2013245 (1983)","journal-title":"IBM Syst. J."},{"key":"16_CR10","doi-asserted-by":"crossref","unstructured":"Boyapati, C., Khurshid, S., Marinov, D.: Korat: automated testing based on java predicates. In: ISSTA, pp. 123\u2013133 (2002)","DOI":"10.1145\/566171.566191"},{"key":"16_CR11","doi-asserted-by":"crossref","unstructured":"Burnim, J., Sen, K.: Heuristics for scalable dynamic test generation. In: ASE, pp. 443\u2013446 (2008)","DOI":"10.1109\/ASE.2008.69"},{"key":"16_CR12","doi-asserted-by":"crossref","unstructured":"Christakis, M., M\u00fcller, P., W\u00fcstholz, V.: Guiding dynamic symbolic execution toward unverified program executions. Technical report, ETH Zurich (2015)","DOI":"10.1145\/2884781.2884843"},{"key":"16_CR13","doi-asserted-by":"crossref","unstructured":"Ciupa, I., Leitner, A., Oriol, M., Meyer, B.: ARTOO: adaptive random testing for object-oriented software. In: Sch\u00e4fer, W., Dwyer, M.B., Gruhn, V. (eds.) ICSE, pp. 71\u201380. ACM (2008)","DOI":"10.1145\/1368088.1368099"},{"key":"16_CR14","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: CAV (2000)","DOI":"10.1007\/10722167_15"},{"key":"16_CR15","doi-asserted-by":"crossref","unstructured":"Csallner, C., Smaragdakis, Y.: Check \u2018n\u2019 crash: combining static checking and testing. In: ICSE, pp. 422\u2013431 (2005)","DOI":"10.1145\/1062455.1062533"},{"issue":"2","key":"16_CR16","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1348250.1348254","volume":"17","author":"C Csallner","year":"2008","unstructured":"Csallner, C., Smaragdakis, Y., Xie, T.: DSD-Crasher: A hybrid analysis tool for bug finding. ACM Trans. Softw. Eng. Methodol. 17(2), 1\u201337 (2008)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"16_CR17","series-title":"Lecture Notes In Computer Science","doi-asserted-by":"crossref","first-page":"100","DOI":"10.1007\/978-3-662-46675-9_7","volume-title":"Fundamental Approaches to Software Engineering","author":"M Czech","year":"2015","unstructured":"Czech, M., Jakobs, M.-C., Wehrheim, H.: Just test what you cannot verify!. In: Egyed, A., Schaefer, I. (eds.) FASE 2015. LNCS, vol. 9033, pp. 100\u2013114. Springer, Heidelberg (2015)"},{"key":"16_CR18","doi-asserted-by":"crossref","unstructured":"Godefroid, P.: Model checking for programming languages using verisoft. In: POPL, pp. 174\u2013186 (1997)","DOI":"10.1145\/263699.263717"},{"key":"16_CR19","doi-asserted-by":"crossref","unstructured":"Godefroid, P.: Compositional dynamic test generation. In: POPL, pp. 47\u201354 (2007)","DOI":"10.1145\/1190215.1190226"},{"key":"16_CR20","unstructured":"Godefroid, P., Levin, M.Y., Molnar, D.A.: Automated whitebox fuzz testing. In: NDSS. The Internet Society (2008)"},{"key":"16_CR21","doi-asserted-by":"crossref","unstructured":"Godefroid, P., Nori, A.V., Rajamani, S.K., Tetali, S.: Compositional may-must program analysis: unleashing the power of alternation. In: POPL, pp. 43\u201356 (2010)","DOI":"10.1145\/1707801.1706307"},{"key":"16_CR22","doi-asserted-by":"crossref","unstructured":"Gulavani, B.S., Henzinger, T.A., Kannan, Y., Nori, A.V., Rajamani, S.K.: Synergy: a new algorithm for property checking. In: SIGSOFT FSE, pp. 117\u2013127 (2006)","DOI":"10.1145\/1181775.1181790"},{"key":"16_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"112","DOI":"10.1007\/11513988_11","volume-title":"Computer Aided Verification","author":"A Gupta","year":"2005","unstructured":"Gupta, A., Strichman, O.: Abstraction refinement for bounded model checking. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 112\u2013124. Springer, Heidelberg (2005)"},{"key":"16_CR24","unstructured":"Gustafsson, J., Betts, A., Ermedahl, A., Lisper, B.: The M\u00e4lardalen WCET benchmarks - past, present and future. In: Lisper, B. (ed.) WCET, pp. 137\u2013147. OCG, Brussels (2010)"},{"key":"16_CR25","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: POPL (2004)","DOI":"10.1145\/964001.964021"},{"issue":"1","key":"16_CR26","doi-asserted-by":"crossref","first-page":"58","DOI":"10.1145\/565816.503279","volume":"37","author":"Thomas A. Henzinger","year":"2002","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: POPL (2002)","journal-title":"ACM SIGPLAN Notices"},{"key":"16_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/978-3-540-70545-1_20","volume-title":"Computer Aided Verification","author":"A Holzer","year":"2008","unstructured":"Holzer, A., Schallhart, C., Tautschnig, M., Veith, H.: FShell: Systematic test case generation for dynamic analysis and measurement. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 209\u2013213. Springer, Heidelberg (2008)"},{"key":"16_CR28","doi-asserted-by":"crossref","unstructured":"Holzer, A., Schallhart, C., Tautschnig, M., Veith, H.: How did you specify your test suite. In: Pecheur, C., Andrews, J., Nitto, E.D. (eds.) ASE, pp. 407\u2013416. ACM (2010)","DOI":"10.1145\/1858996.1859084"},{"issue":"1","key":"16_CR29","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1016\/j.entcs.2005.07.021","volume":"144","author":"D Kroening","year":"2006","unstructured":"Kroening, D.: Computing over-approximations with bounded model checking. Electr. Notes Theor. Comput. Sci. 144(1), 79\u201392 (2006)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"16_CR30","doi-asserted-by":"crossref","unstructured":"Majumdar, R., Sen, K.: Hybrid concolic testing. In: ICSE, ICSE 2007, pp. 416\u2013426. IEEE Computer Society, Washington, DC (2007)","DOI":"10.1109\/ICSE.2007.41"},{"key":"16_CR31","unstructured":"Majumdar, R., Sen, K.: Latest : Lazy dynamic test input generation. Technical Report UCB\/EECS-2007-36, EECS Department, University of California, Berkeley (2007)"},{"key":"16_CR32","doi-asserted-by":"crossref","unstructured":"Pacheco, C., Lahiri, S.K., Ernst, M.D., Ball, T.: Feedback-directed random test generation. In: ICSE, pp. 75\u201384. IEEE Computer Society (2007)","DOI":"10.1109\/ICSE.2007.37"},{"key":"16_CR33","doi-asserted-by":"crossref","unstructured":"Klarlund, N., Godefroid, P., Sen, K.: DART: directed automated random testing. In: PLDI, pp. 213\u2013223. ACM (2005)","DOI":"10.1145\/1064978.1065036"},{"key":"16_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/978-3-642-02652-2_16","volume-title":"Model Checking Software","author":"N Rungta","year":"2009","unstructured":"Rungta, N., Mercer, E.G., Visser, W.: Efficient testing of concurrent programs with abstraction-guided symbolic execution. In: P\u0103s\u0103reanu, C.S. (ed.) Model Checking Software. LNCS, vol. 5578, pp. 174\u2013191. Springer, Heidelberg (2009)"},{"key":"16_CR35","doi-asserted-by":"crossref","unstructured":"Sen, K., Marinov, D., Agha, G.: CUTE: a concolic unit testing engine for C. In: ESEC\/SIGSOFT FSE, pp. 263\u2013272 (2005)","DOI":"10.21236\/ADA482657"},{"key":"16_CR36","doi-asserted-by":"crossref","unstructured":"Visser, W., Pasareanu, C.S., Khurshid, S.: Test input generation with Java PathFinder. In: Avrunin, G.S., Rothermel, G. (eds.) ISSTA, pp. 97\u2013107. ACM (2004)","DOI":"10.1145\/1013886.1007526"},{"key":"16_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1007\/978-3-540-31980-1_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T Xie","year":"2005","unstructured":"Xie, T., Marinov, D., Schulte, W., Notkin, D.: Symstra: a framework for generating object-oriented unit tests using symbolic execution. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 365\u2013381. Springer, Heidelberg (2005)"}],"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_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,31]],"date-time":"2025-05-31T22:49:42Z","timestamp":1748731782000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-49122-5_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,12,25]]},"ISBN":["9783662491218","9783662491225"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-49122-5_16","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"}}]}}