{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T02:09:33Z","timestamp":1776305373866,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":35,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783662496732","type":"print"},{"value":"9783662496749","type":"electronic"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"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":[[2016]]},"DOI":"10.1007\/978-3-662-49674-9_26","type":"book-chapter","created":{"date-parts":[[2016,4,8]],"date-time":"2016-04-08T14:49:00Z","timestamp":1460126940000},"page":"442-459","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":55,"title":["JDart: A Dynamic Symbolic Analysis Framework"],"prefix":"10.1007","author":[{"given":"Kasper","family":"Luckow","sequence":"first","affiliation":[]},{"given":"Marko","family":"Dimja\u0161evi\u0107","sequence":"additional","affiliation":[]},{"given":"Dimitra","family":"Giannakopoulou","sequence":"additional","affiliation":[]},{"given":"Falk","family":"Howar","sequence":"additional","affiliation":[]},{"given":"Malte","family":"Isberner","sequence":"additional","affiliation":[]},{"given":"Temesghen","family":"Kahsai","sequence":"additional","affiliation":[]},{"given":"Zvonimir","family":"Rakamari\u0107","sequence":"additional","affiliation":[]},{"given":"Vishwanath","family":"Raman","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,4,9]]},"reference":[{"key":"26_CR1","unstructured":"ASM: A Java bytecode engineering library. \n                      http:\/\/asm.ow2.org"},{"key":"26_CR2","doi-asserted-by":"crossref","unstructured":"Balasubramanian, D., P\u0103s\u0103reanu, C.S., Whalen, M.W., Karsai, G., Lowry, M.: Polyglot: modeling and analysis for multiple statechart formalisms. In: Proceedings of the International Symposium on Software Testing and Analysis (ISSTA), pp. 45\u201355 (2011)","DOI":"10.1145\/2001420.2001427"},{"key":"26_CR3","unstructured":"Cadar, C., Dunbar, D., Engler, D.: KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. In: Proceedings of the 5th USENIX Symposium on Operating Systems Design and Implementation (OSDI), pp. 209\u2013224 (2008)"},{"key":"26_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"248","DOI":"10.1007\/978-3-642-31759-0_19","volume-title":"Model Checking Software","author":"J Christ","year":"2012","unstructured":"Christ, J., Hoenicke, J., Nutz, A.: SMTInterpol: an interpolating SMT solver. In: Donaldson, A., Parker, D. (eds.) SPIN 2012. LNCS, vol. 7385, pp. 248\u2013254. Springer, Heidelberg (2012)"},{"key":"26_CR5","doi-asserted-by":"crossref","unstructured":"Deters, M., Reynolds, A., King, T., Barrett, C.W., Tinelli, C.: A tour of CVC4: how it works, and how to use it. In: Proceedings of the 14th Conference on Formal Methods in Computer-Aided Design (FMCAD), p. 7 (2014)","DOI":"10.1109\/FMCAD.2014.6987586"},{"issue":"1","key":"26_CR6","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/2693208.2693248","volume":"40","author":"M 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: concolic execution in java pathfinder and its applications. ACM SIGSOFT Softw. Eng. Notes 40(1), 1\u20135 (2015). Proceedings of the 2014 Java Pathfinder Workshop (JPF)","journal-title":"ACM SIGSOFT Softw. Eng. Notes"},{"key":"26_CR7","unstructured":"Dimja\u0161evi\u0107, M., Rakamari\u0107, Z.: JPF-Doop: combining concolic and random testing for java. In: Java Pathfinder Workshop (JPF) (2013) (Extended abstract)"},{"key":"26_CR8","doi-asserted-by":"crossref","unstructured":"Dinges, P., Agha, G.: Solving complex path conditions through heuristic search on induced polytopes. In: Proceedings of the 22nd ACM SIGSOFT International Symposium on Foundations of Software Engineering (FSE), pp. 425\u2013436 (2014)","DOI":"10.1145\/2635868.2635889"},{"key":"26_CR9","unstructured":"Erzberger, H., Lauderdale, T.A., Chu, Y.C.: Automated conflict resolution, arrival management and weather avoidance for ATM. In: International Congress of the Aeronautical Sciences (2010)"},{"key":"26_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"208","DOI":"10.1007\/978-3-642-38574-2_14","volume-title":"Automated Deduction \u2013 CADE-24","author":"S Gao","year":"2013","unstructured":"Gao, S., Kong, S., Clarke, E.M.: dReal: an SMT solver for nonlinear theories over the reals. In: Bonacina, M.P. (ed.) CADE 2013. LNCS, vol. 7898, pp. 208\u2013214. Springer, Heidelberg (2013)"},{"key":"26_CR11","unstructured":"Gario, M., Micheli, A.: pysmt: a solver-agnostic library for fast prototyping of SMT-based algorithms. In: Proceedings of the 13th International Workshop on Satisfiability Modulo Theories (SMT) (2015)"},{"key":"26_CR12","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 (2014)","DOI":"10.1145\/2642937.2642940"},{"key":"26_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"248","DOI":"10.1007\/978-3-642-33125-1_18","volume-title":"Static Analysis","author":"D Giannakopoulou","year":"2012","unstructured":"Giannakopoulou, D., Rakamari\u0107, Z., Raman, V.: Symbolic learning of component interfaces. In: Min\u00e9, A., Schmidt, D. (eds.) SAS 2012. LNCS, vol. 7460, pp. 248\u2013264. Springer, Heidelberg (2012)"},{"key":"26_CR14","doi-asserted-by":"crossref","unstructured":"Godefroid, P., Klarlund, N., Sen, K.: DART: directed automated random testing. In: Proceedings of the 26th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pp. 213\u2013223 (2005)","DOI":"10.1145\/1064978.1065036"},{"issue":"3","key":"26_CR15","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1145\/2093548.2093564","volume":"55","author":"P Godefroid","year":"2012","unstructured":"Godefroid, P., Levin, M.Y., Molnar, D.: SAGE: whitebox fuzzing for security testing. Commun. ACM 55(3), 40\u201344 (2012)","journal-title":"Commun. ACM"},{"key":"26_CR16","doi-asserted-by":"crossref","unstructured":"Howar, F., Giannakopoulou, D., Rakamari\u0107, Z.: Hybrid learning: interface generation through static, dynamic, and symbolic analysis. In: Proceedings of the International Symposium on Software Testing and Analysis (ISSTA), pp. 268\u2013279 (2013)","DOI":"10.1145\/2483760.2483783"},{"key":"26_CR17","unstructured":"JaCoCo Java code coverage library. \n                      http:\/\/www.eclemma.org\/jacoco"},{"key":"26_CR18","unstructured":"Jayaraman, K., Harvison, D., Ganesh, V.: jFuzz: a concolic whitebox fuzzer for Java. In: Proceedings of the 1st NASA Formal Methods Symposium (NFM), pp. 121\u2013125 (2009)"},{"key":"26_CR19","unstructured":"Java Pathfinder. \n                      http:\/\/jpf.byu.edu"},{"key":"26_CR20","unstructured":"K\u00e4hk\u00f6nen, K., Launiainen, T., Saarikivi, O., Kauttio, J., Heljanko, K., Niemel\u00e4, I.: LCT: an open source concolic testing tool for Java programs. In: Proceedings of the 6th Workshop on Bytecode Semantics, Verification, Analysis and Transformation (BYTECODE), pp. 75\u201380 (2011)"},{"key":"26_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":"26_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":"26_CR23","doi-asserted-by":"crossref","unstructured":"Pacheco, C., Lahiri, S., Ernst, M., Ball, T.: Feedback-directed random test generation. In: Proceedings of the 29th International Conference on Software Engineering (ICSE), pp. 75\u201384 (2007)","DOI":"10.1109\/ICSE.2007.37"},{"key":"26_CR24","doi-asserted-by":"crossref","unstructured":"Pasareanu, C.S., Rungta, N., Visser, W.: Symbolic execution with mixed concrete-symbolic solving. In: Proceedings of the International Symposium on Software Testing and Analysis (ISSTA), pp. 34\u201344 (2011)","DOI":"10.1145\/2001420.2001425"},{"key":"26_CR25","doi-asserted-by":"crossref","unstructured":"P\u01ces\u01cereanu, C.S., Mehlitz, P.C., Bushnell, D.H., Gundy-Burlet, K., Lowry, M., Person, S., Pape, M.: Combining unit-level symbolic execution and system-level concrete execution for testing NASA software. In: Proceedings of the International Symposium on Software Testing and Analysis (ISSTA), pp. 15\u201326 (2008)","DOI":"10.1145\/1390630.1390635"},{"key":"26_CR26","doi-asserted-by":"crossref","unstructured":"Qiu, R., Yang, G., P\u0103s\u0103reanu, C.S., Khurshid, S.: Compositional symbolic execution with memoized replay. In: Proceedings of the 37th International Conference on Software Engineering (ICSE), pp. 632\u2013642 (2015)","DOI":"10.1109\/ICSE.2015.79"},{"key":"26_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"419","DOI":"10.1007\/11817963_38","volume-title":"Computer Aided Verification","author":"K Sen","year":"2006","unstructured":"Sen, K., Agha, G.: CUTE and jCUTE: concolic unit testing and explicit path model-checking tools. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 419\u2013423. Springer, Heidelberg (2006)"},{"key":"26_CR28","doi-asserted-by":"crossref","unstructured":"Sen, K., Marinov, D., Agha, G.: CUTE: a concolic unit testing engine for C. In: Proceedings of the 10th European Software Engineering Conference Held Jointly with 13th ACM SIGSOFT International Symposium on Foundations of Software Engineering (ESEC\/FSE), pp. 263\u2013272 (2005)","DOI":"10.1145\/1081706.1081750"},{"key":"26_CR29","unstructured":"The SMT-LIB standard. \n                      http:\/\/smtlib.cs.uiowa.edu"},{"key":"26_CR30","unstructured":"Soot: A Java optimization framework. \n                      http:\/\/sable.github.io\/soot"},{"key":"26_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/978-3-642-20398-5_26","volume-title":"NASA Formal Methods","author":"M Souza","year":"2011","unstructured":"Souza, M., Borges, M., d\u2019Amorim, M., P\u0103s\u0103reanu, C.S.: CORAL: solving complex constraints for symbolic pathfinder. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 359\u2013374. Springer, Heidelberg (2011)"},{"key":"26_CR32","doi-asserted-by":"crossref","unstructured":"Staats, M., P\u01ces\u01cereanu, C.: Parallel symbolic execution for structural test generation. In: Proceedings of the International Symposium on Software Testing and Analysis (ISSTA), pp. 183\u2013194 (2010)","DOI":"10.1145\/1831708.1831732"},{"key":"26_CR33","doi-asserted-by":"crossref","unstructured":"Tanno, H., Zhang, X., Hoshino, T., Sen, K.: TesMa and CATG: automated test generation tools for models of enterprise applications. In: Proceedings of the 37th International Conference on Software Engineering (ICSE), pp. 717\u2013720 (2015)","DOI":"10.1109\/ICSE.2015.231"},{"key":"26_CR34","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":"N Tillmann","year":"2008","unstructured":"Tillmann, N., de Halleux, J.: Pex\u2013White box test generation for\u00a0.NET. In: Beckert, B., H\u00e4hnle, R. (eds.) TAP 2008. LNCS, vol. 4966, pp. 134\u2013153. Springer, Heidelberg (2008)"},{"issue":"2","key":"26_CR35","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1023\/A:1022920129859","volume":"10","author":"W Visser","year":"2003","unstructured":"Visser, W., Havelund, K., Brat, G.P., Park, S., Lerda, F.: Model checking programs. Autom. Softw. Eng. 10(2), 203\u2013232 (2003)","journal-title":"Autom. Softw. Eng."}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-49674-9_26","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,3,23]],"date-time":"2020-03-23T21:14:18Z","timestamp":1584998058000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-49674-9_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783662496732","9783662496749"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-49674-9_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"9 April 2016","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}