{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,6]],"date-time":"2026-04-06T10:08:03Z","timestamp":1775470083297,"version":"3.50.1"},"reference-count":22,"publisher":"Springer Science and Business Media LLC","issue":"6","license":[{"start":{"date-parts":[[2020,6,2]],"date-time":"2020-06-02T00:00:00Z","timestamp":1591056000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2020,6,2]],"date-time":"2020-06-02T00:00:00Z","timestamp":1591056000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100000761","name":"Imperial College London","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100000761","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2021,12]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>KLEE is a popular dynamic symbolic execution engine, initially designed at Stanford University and now primarily developed and maintained by the Software Reliability Group at Imperial College London. KLEE has a large community spanning both academia and industry, with over 60 contributors on GitHub, over 350 subscribers on its mailing list, and over 80 participants to a recent dedicated workshop. KLEE has been used and extended by groups from many universities and companies in a variety of different areas such as high-coverage test generation, automated debugging, exploit generation, wireless sensor networks, and online gaming, among many others.\n<\/jats:p>","DOI":"10.1007\/s10009-020-00570-3","type":"journal-article","created":{"date-parts":[[2020,6,2]],"date-time":"2020-06-02T15:07:47Z","timestamp":1591110467000},"page":"867-870","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":32,"title":["KLEE symbolic execution engine in 2019"],"prefix":"10.1007","volume":"23","author":[{"given":"Cristian","family":"Cadar","sequence":"first","affiliation":[]},{"given":"Martin","family":"Nowack","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2020,6,2]]},"reference":[{"key":"570_CR1","doi-asserted-by":"crossref","unstructured":"Barrett, C., Conway, C., Deters, M., Hadarean, L., Jovanovic, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Proceedings of the 23rd International Conference on Computer-Aided Verification (CAV\u201911) (2011)","DOI":"10.1007\/978-3-642-22110-1_14"},{"key":"570_CR2","doi-asserted-by":"crossref","unstructured":"Boyer, R.S., Elspas, B., Levitt, K.N.: Select\u2014a formal system for testing and debugging programs by symbolic execution. In: Proceedings of the International Conference on Reliable Software (ICRS\u201975) (1975)","DOI":"10.1145\/800027.808445"},{"key":"570_CR3","doi-asserted-by":"crossref","unstructured":"Brummayer, R., Biere, A.: Boolector: an efficient SMT solver for bit-vectors and arrays. In: Proceedings of the 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201909) (2009)","DOI":"10.1007\/978-3-642-00768-2_16"},{"key":"570_CR4","doi-asserted-by":"crossref","unstructured":"Bucur, S., Ureche, V., Zamfir, C., Candea, G.: Parallel symbolic execution for automated real-world software testing. In: Proceedings of the 6th European Conference on Computer Systems (EuroSys\u201911) (2011)","DOI":"10.1145\/1966445.1966463"},{"key":"570_CR5","unstructured":"Cadar, C., Dunbar, D., Engler, D.: KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. In: Proceedings of the 8th USENIX Symposium on Operating Systems Design and Implementation (OSDI\u201908) (2008)"},{"key":"570_CR6","doi-asserted-by":"crossref","unstructured":"Cadar, C., Engler, D.: Execution generated test cases: how to make systems code crash itself. In: Proceedings of the 12th International SPIN Workshop on Model Checking of Software (SPIN\u201905) (2005)","DOI":"10.1007\/11537328_2"},{"key":"570_CR7","doi-asserted-by":"crossref","unstructured":"Cadar, C., Ganesh, V., Pawlowski, P., Dill, D., Engler, D.: EXE: automatically generating inputs of death. In: Proceedings of the 13th ACM Conference on Computer and Communications Security (CCS\u201906) (2006)","DOI":"10.1145\/1180405.1180445"},{"issue":"2","key":"570_CR8","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1145\/2408776.2408795","volume":"56","author":"C Cadar","year":"2013","unstructured":"Cadar, C., Sen, K.: Symbolic execution for software testing: three decades later. Commun. Assoc. Comput. Mach. (CACM) 56(2), 82\u201390 (2013)","journal-title":"Commun. Assoc. Comput. Mach. (CACM)"},{"key":"570_CR9","doi-asserted-by":"crossref","unstructured":"Clarke, L.A.: A program testing system. In: Proceedings of the 1976 Annual Conference (ACM\u201976) (1976)","DOI":"10.1145\/800191.805647"},{"key":"570_CR10","doi-asserted-by":"crossref","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201908) (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"570_CR11","doi-asserted-by":"crossref","unstructured":"Dutertre, B.: Yices 2.2. In: Proceedings of the 26th International Conference on Computer-Aided Verification (CAV\u201914) (2014)","DOI":"10.1007\/978-3-319-08867-9_49"},{"key":"570_CR12","unstructured":"Ganesh, V., Dill, D.L.: A decision procedure for bit-vectors and arrays. In: Proceedings of the 19th International Conference on Computer-Aided Verification (CAV\u201907) (2007)"},{"key":"570_CR13","doi-asserted-by":"crossref","unstructured":"Godefroid, P., Klarlund, N., Sen, K.: DART: directed automated random testing. In: Proceedings of the Conference on Programing Language Design and Implementation (PLDI\u201905) (2005)","DOI":"10.1145\/1065010.1065036"},{"key":"570_CR14","unstructured":"Haedicke, F., Frehse, S., Fey, G., Gro\u00dfe, D., Drechsler, R.: metaSMT: focus on your application not on solver integration. In: Proceedings of the International Workshop on Design and Implementation of Formal Tools and Systems (DIFTS\u201912) (2011)"},{"key":"570_CR15","doi-asserted-by":"crossref","unstructured":"King, J.C.: A new approach to program testing. In: Proceedings of the International Conference on Reliable Software (ICRS\u201975) (1975)","DOI":"10.1145\/800027.808444"},{"key":"570_CR16","unstructured":"Lattner, C., Adve, V.: LLVM: a compilation framework for lifelong program analysis & transformation. In: Proceedings of the 2nd International Symposium on Code Generation and Optimization (CGO\u201904) (2004)"},{"key":"570_CR17","doi-asserted-by":"crossref","unstructured":"Li, G., Ghosh, I., Rajan, S.P.: KLOVER: a symbolic execution and automatic test generation tool for C++ programs. In: Proceedings of the 23rd International Conference on Computer-Aided Verification (CAV\u201911) (2011)","DOI":"10.1007\/978-3-642-22110-1_49"},{"key":"570_CR18","doi-asserted-by":"crossref","unstructured":"Li, G., Li, P., Sawaga, G., Gopalakrishnan, G., Ghosh, I., Rajan, S.P.: GKLEE: concolic verification and test generation for GPUs. In: Proceedings of the 17th ACM Symposium on Principles and Practice of Parallel Programming (PPoPP\u201912) (2012)","DOI":"10.1145\/2145816.2145844"},{"key":"570_CR19","doi-asserted-by":"crossref","unstructured":"Liew, D., Schemmel, D., Cadar, C., Donaldson, A., Z\u00e4hl, R., Wehrle, K.: Floating-point symbolic execution: a case study in n-version programming. In: Proceedings of the 32nd IEEE International Conference on Automated Software Engineering (ASE\u201917) (2017)","DOI":"10.1109\/ASE.2017.8115670"},{"key":"570_CR20","doi-asserted-by":"crossref","unstructured":"Palikareva, H., Cadar, C.: Multi-solver support in symbolic execution. In: Proceedings of the 25th International Conference on Computer-Aided Verification (CAV\u201913) (2013)","DOI":"10.1007\/978-3-642-39799-8_3"},{"key":"570_CR21","doi-asserted-by":"crossref","unstructured":"Perry, D.M., Mattavelli, A., Zhang, X., Cadar, C.: Accelerating array constraints in symbolic execution. In: Proceedings of the International Symposium on Software Testing and Analysis (ISSTA\u201917) (2017)","DOI":"10.1145\/3092703.3092728"},{"key":"570_CR22","doi-asserted-by":"crossref","unstructured":"Sasnauskas, R., Landsiedel, O., Alizai, M.H., Weise, C., Kowalewski, S., Wehrle, K.: Kleenet: discovering insidious interaction bugs in wireless sensor networks before deployment. In: Proceedings of the 9th ACM\/IEEE International Conference on Information Processing in Sensor Networks (IPSN\u201910) (2010)","DOI":"10.1145\/1791212.1791235"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-020-00570-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10009-020-00570-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-020-00570-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,12,26]],"date-time":"2021-12-26T12:02:34Z","timestamp":1640520154000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10009-020-00570-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,6,2]]},"references-count":22,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2021,12]]}},"alternative-id":["570"],"URL":"https:\/\/doi.org\/10.1007\/s10009-020-00570-3","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,6,2]]},"assertion":[{"value":"2 June 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}