{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,22]],"date-time":"2026-09-22T21:27:54Z","timestamp":1790112474266,"version":"4.0.1"},"publisher-location":"Cham","reference-count":28,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319026534","type":"print"},{"value":"9783319026541","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-319-02654-1_16","type":"book-chapter","created":{"date-parts":[[2013,10,21]],"date-time":"2013-10-21T01:25:32Z","timestamp":1382318732000},"page":"281-301","source":"Crossref","is-referenced-by-count":15,"title":["A Generic Framework for Symbolic Execution"],"prefix":"10.1007","author":[{"given":"Andrei","family":"Arusoaie","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Dorel","family":"Lucanu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Vlad","family":"Rusu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"16_CR1","doi-asserted-by":"crossref","unstructured":"Armando, A., Benerecetti, M., Mantovani, J.: Model checking linear programs with arrays. In: Proceedings of the Workshop on Software Model Checking, vol.\u00a0144-3, pp. 79\u201394 (2006)","DOI":"10.1016\/j.entcs.2006.01.006"},{"key":"16_CR2","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139172752","volume-title":"Term rewriting and all that","author":"F. Baader","year":"1998","unstructured":"Baader, F., Nipkow, T.: Term rewriting and all that. Cambridge University Press, New York (1998)"},{"key":"16_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/11575467_5","volume-title":"Programming Languages and Systems","author":"J. Berdine","year":"2005","unstructured":"Berdine, J., Calcagno, C., O\u2019Hearn, P.W.: Symbolic execution with separation logic. In: Yi, K. (ed.) APLAS 2005. LNCS, vol.\u00a03780, pp. 52\u201368. Springer, Heidelberg (2005)"},{"key":"16_CR4","doi-asserted-by":"crossref","unstructured":"Cadar, C., Ganesh, V., Pawlowski, P.M., Dill, D.L., Engler, D.R.: EXE: automatically generating inputs of death. In: Juels, A., Wright, R.N., di Vimercati, S.D.C. (eds.) ACM Conference on Computer and Communications Security, pp. 322\u2013335. ACM (2006)","DOI":"10.1145\/1180405.1180445"},{"key":"16_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-540-79124-9_12","volume-title":"Tests and Proofs","author":"J. Halleux de","year":"2008","unstructured":"de Halleux, J., Tillmann, N.: Parameterized unit testing with pex. In: Beckert, B., H\u00e4hnle, R. (eds.) TAP 2008. LNCS, vol.\u00a04966, pp. 171\u2013181. Springer, Heidelberg (2008)"},{"key":"16_CR6","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.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"issue":"1","key":"16_CR7","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1109\/32.44363","volume":"16","author":"L.K. Dillon","year":"1990","unstructured":"Dillon, L.K.: Verifying general safety properties of Ada tasking programs. IEEE Trans. Softw. Eng.\u00a016(1), 51\u201363 (1990)","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"3","key":"16_CR8","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1016\/j.entcs.2009.05.015","volume":"238","author":"S. Escobar","year":"2009","unstructured":"Escobar, S., Meseguer, J., Sasse, R.: Variant narrowing and equational unification. Electr. Notes Theor. Comput. Sci.\u00a0238(3), 103\u2013119 (2009)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"16_CR9","doi-asserted-by":"crossref","unstructured":"Godefroid, P., Klarlund, N., Sen, K.: DART: directed automated random testing. In: PLDI, pp. 213\u2013223. ACM (2005)","DOI":"10.1145\/1064978.1065036"},{"key":"16_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/978-3-540-73449-9_19","volume-title":"Term Rewriting and Applications","author":"M. Hills","year":"2007","unstructured":"Hills, M., Ro\u015fu, G.: KOOL: An application of rewriting logic to language prototyping and analysis. In: Baader, F. (ed.) RTA 2007. LNCS, vol.\u00a04533, pp. 246\u2013256. Springer, Heidelberg (2007)"},{"key":"16_CR11","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.\u00a02619, pp. 553\u2013568. Springer, Heidelberg (2003)"},{"issue":"7","key":"16_CR12","doi-asserted-by":"publisher","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\u00a019(7), 385\u2013394 (1976)","journal-title":"Commun. ACM"},{"key":"16_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"609","DOI":"10.1007\/978-3-642-22110-1_49","volume-title":"Computer Aided Verification","author":"G. Li","year":"2011","unstructured":"Li, G., Ghosh, I., Rajan, S.P.: KLOVER: A symbolic execution and automatic test generation tool for C++ programs. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 609\u2013615. Springer, Heidelberg (2011)"},{"key":"16_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"362","DOI":"10.1007\/978-3-642-38613-8_25","volume-title":"Integrated Formal Methods","author":"D. Lucanu","year":"2013","unstructured":"Lucanu, D., Rusu, V.: Program equivalence by circular reasoning. In: Johnsen, E.B., Petre, L. (eds.) IFM 2013. LNCS, vol.\u00a07940, pp. 362\u2013377. Springer, Heidelberg (2013)"},{"key":"16_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/978-3-642-34005-5_3","volume-title":"Rewriting Logic and Its Applications","author":"D. Lucanu","year":"2012","unstructured":"Lucanu, D., \u015eerb\u0103nu\u0163\u0103, T.F., Ro\u015fu, G.: \n                    \n                      \n                    \n                    $\\mathbb{K}$\n                   Framework Distilled. In: Dur\u00e1n, F. (ed.) WRLA 2012. LNCS, vol.\u00a07571, pp. 31\u201353. Springer, Heidelberg (2012)"},{"key":"16_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/10721975_1","volume-title":"Rewriting Techniques and Applications","author":"J. Meseguer","year":"2000","unstructured":"Meseguer, J.: Rewriting logic and Maude: Concepts and applications. In L.\u00a0Bachmair, editor, RTA. In: Bachmair, L. (ed.) RTA 2000. LNCS, vol.\u00a01833, pp. 1\u201326. Springer, Heidelberg (2000)"},{"issue":"1-2","key":"16_CR17","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/s10990-007-9000-6","volume":"20","author":"J. Meseguer","year":"2007","unstructured":"Meseguer, J., Thati, P.: Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols. Higher-Order and Symbolic Computation\u00a020(1-2), 123\u2013160 (2007)","journal-title":"Higher-Order and Symbolic Computation"},{"key":"16_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"164","DOI":"10.1007\/978-3-540-24732-6_13","volume-title":"Model Checking Software","author":"C.S. P\u0103s\u0103reanu","year":"2004","unstructured":"P\u0103s\u0103reanu, C.S., Visser, W.: Verification of Java Programs Using Symbolic Execution and Invariant Generation. In: Graf, S., Mounier, L. (eds.) SPIN 2004. LNCS, vol.\u00a02989, pp. 164\u2013181. Springer, Heidelberg (2004)"},{"issue":"4","key":"16_CR19","doi-asserted-by":"publisher","first-page":"339","DOI":"10.1007\/s10009-009-0118-1","volume":"11","author":"C.S. P\u0103s\u0103reanu","year":"2009","unstructured":"P\u0103s\u0103reanu, C.S., Visser, W.: A survey of new trends in symbolic execution for software testing and analysis. STTT\u00a011(4), 339\u2013353 (2009)","journal-title":"STTT"},{"issue":"6","key":"16_CR20","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1016\/j.jlap.2010.03.012","volume":"79","author":"G. Ro\u015fu","year":"2010","unstructured":"Ro\u015fu, G., \u015eerb\u0103nu\u0163\u0103, T.F.: An overview of the K semantic framework. Journal of Logic and Algebraic Programming\u00a079(6), 397\u2013434 (2010)","journal-title":"Journal of Logic and Algebraic Programming"},{"key":"16_CR21","doi-asserted-by":"crossref","unstructured":"Ro\u015fu, G., \u015etef\u0103nescu, A.: Checking reachability using matching logic. In: Leavens, G.T., Dwyer, M.B. (eds.) OOPSLA, pp. 555\u2013574. ACM (2012)","DOI":"10.1145\/2398857.2384656"},{"key":"16_CR22","unstructured":"Schmitt, P.H., Wei\u00df, B.: Inferring invariants by symbolic execution. In: Proceedings of 4th International Verification Workshop, VERIFY 2007 (2007)"},{"key":"16_CR23","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-13, pp. 263\u2013272. ACM (2005)","DOI":"10.1145\/1081706.1081750"},{"key":"16_CR24","unstructured":"Serbanuta, T.F., Arusoaie, A., Lazar, D., Ellison, C., Lucanu, D., Rosu, G.: The K primer (version 2.5). In: Hills, M. (ed.) K 2011. Electronic Notes in Theoretical Computer Science (2011) (to appear)"},{"issue":"2","key":"16_CR25","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1016\/j.ic.2008.03.026","volume":"207","author":"T.-F. \u015eerb\u0103nu\u0163\u0103","year":"2009","unstructured":"\u015eerb\u0103nu\u0163\u0103, T.-F., Ro\u015fu, G., Meseguer, J.: A rewriting logic approach to operational semantics. Inf. Comput.\u00a0207(2), 305\u2013340 (2009)","journal-title":"Inf. Comput."},{"key":"16_CR26","doi-asserted-by":"crossref","unstructured":"Siegel, S.F., Mironova, A., Avrunin, G.S., Clarke, L.A.: Using model checking with symbolic execution to verify parallel numerical programs. In: ISSTA, pp. 157\u2013168. ACM (2006)","DOI":"10.1145\/1146238.1146256"},{"key":"16_CR27","doi-asserted-by":"crossref","unstructured":"Staats, M., P\u0103s\u0103reanu, C.S.: Parallel symbolic execution for structural test generation. In: Tonella, P., Orso, A. (eds.) ISSTA, pp. 183\u2013194. ACM (2010)","DOI":"10.1145\/1831708.1831732"},{"key":"16_CR28","doi-asserted-by":"crossref","unstructured":"Visser, W., P\u0103s\u0103reanu, 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"}],"container-title":["Lecture Notes in Computer Science","Software Language Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-02654-1_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,23]],"date-time":"2019-05-23T17:19:05Z","timestamp":1558631945000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-02654-1_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783319026534","9783319026541"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-02654-1_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013]]}}}