{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T09:57:59Z","timestamp":1776333479257,"version":"3.51.2"},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642397981","type":"print"},{"value":"9783642397998","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-39799-8_3","type":"book-chapter","created":{"date-parts":[[2013,7,10]],"date-time":"2013-07-10T19:13:06Z","timestamp":1373483586000},"page":"53-68","source":"Crossref","is-referenced-by-count":52,"title":["Multi-solver Support in Symbolic Execution"],"prefix":"10.1007","author":[{"given":"Hristina","family":"Palikareva","sequence":"first","affiliation":[]},{"given":"Cristian","family":"Cadar","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"3_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/978-3-642-00768-2_16","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R. Brummayer","year":"2009","unstructured":"Brummayer, R., Biere, A.: Boolector: An efficient SMT solver for bit-vectors and arrays. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol.\u00a05505, pp. 174\u2013177. Springer, Heidelberg (2009)"},{"key":"3_CR2","unstructured":"Cadar, C., Dunbar, D., Engler, D.: KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs. In: OSDI 2008 (2008)"},{"key":"3_CR3","doi-asserted-by":"crossref","unstructured":"Cadar, C., Ganesh, V., Pawlowski, P., Dill, D., Engler, D.: EXE: Automatically generating inputs of death. In: CCS 2006 (2006)","DOI":"10.1145\/1180405.1180445"},{"key":"3_CR4","doi-asserted-by":"crossref","unstructured":"Cadar, C., Godefroid, P., Khurshid, S., Pasareanu, C., Sen, K., Tillmann, N., Visser, W.: Symbolic execution for software testing in practice\u2014preliminary assessment. In: ICSE Impact 2011 (2011)","DOI":"10.1145\/1985793.1985995"},{"key":"3_CR5","doi-asserted-by":"crossref","unstructured":"Cadar, C., Pietzuch, P., Wolf, A.L.: Multiplicity computing: A vision of software engineering for next-generation computing platform applications. In: FoSER 2010 (2010)","DOI":"10.1145\/1882362.1882380"},{"issue":"2","key":"3_CR6","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. ACM\u00a056(2), 82\u201390 (2013)","journal-title":"Commun. ACM"},{"key":"3_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/978-3-540-24730-2_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E. Clarke","year":"2004","unstructured":"Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 168\u2013176. Springer, Heidelberg (2004)"},{"key":"3_CR8","unstructured":"Cledat, R., Kumar, T., Sreeram, J., Pande, S.: Opportunistic computing: A new paradigm for scalable realism on many-cores. In: HotPar 2009 (2009)"},{"key":"3_CR9","doi-asserted-by":"crossref","unstructured":"Cordeiro, L., Fischer, B., Marques-Silva, J.: SMT-based bounded model checking for embedded ANSI-C software. In: ASE 2009 (2009)","DOI":"10.1109\/ASE.2009.63"},{"issue":"9","key":"3_CR10","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1145\/1995376.1995394","volume":"54","author":"L. Moura De","year":"2011","unstructured":"De Moura, L., Bj\u00f8rner, N.: Satisfiability modulo theories: introduction and applications. Commun. ACM\u00a054(9), 69\u201377 (2011)","journal-title":"Commun. ACM"},{"key":"3_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"519","DOI":"10.1007\/978-3-540-73368-3_52","volume-title":"Computer Aided Verification","author":"V. Ganesh","year":"2007","unstructured":"Ganesh, V., Dill, D.L.: A decision procedure for bit-vectors and arrays. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 519\u2013531. Springer, Heidelberg (2007)"},{"key":"3_CR12","unstructured":"Haedicke, F., Frehse, S., Fey, G., Gro\u00dfe, D., Drechsler, R.: metaSMT: Focus on your application not on solver integration. In: DIFTS 2012 (2012)"},{"key":"3_CR13","first-page":"245","volume":"6","author":"Y. Hamadi","year":"2009","unstructured":"Hamadi, Y., Sais, L.: ManySAT: a parallel SAT solver. JSAT\u00a06, 245\u2013262 (2009)","journal-title":"JSAT"},{"issue":"7","key":"3_CR14","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. CACM\u00a019(7), 385\u2013394 (1976)","journal-title":"CACM"},{"key":"3_CR15","unstructured":"Lattner, C., Adve, V.: LLVM: A compilation framework for lifelong program analysis & transformation. In: CGO 2004 (2004)"},{"key":"3_CR16","unstructured":"Marinescu, P.D., Cadar, C.: make test-zesti: A symbolic execution solution for improving regression testing. In: ICSE 2012 (2012)"},{"key":"3_CR17","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.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"3_CR18","unstructured":"Ranise, S., Tinelli, C.: The SMT-LIB format: An initial proposal. In: PDPAR 2003 (2003)"},{"key":"3_CR19","doi-asserted-by":"crossref","unstructured":"Sen, K., Marinov, D., Agha, G.: CUTE: A concolic unit testing engine for C. In: ESEC\/FSE 2005 (2005)","DOI":"10.21236\/ADA482657"},{"key":"3_CR20","doi-asserted-by":"crossref","unstructured":"Trachsel, O., Gross, T.R.: Variant-based competitive parallel execution of sequential programs. In: CF 2010 (2010)","DOI":"10.1145\/1787275.1787325"},{"key":"3_CR21","unstructured":"Vajda, A., Stenstrom, P.: Semantic information based speculative parallel execution. In: PESPMA 2010 (2010)"},{"key":"3_CR22","doi-asserted-by":"crossref","unstructured":"Visser, W., Geldenhuys, J., Dwyer, M.B.: Green: reducing, reusing and recycling constraints in program analysis. In: FSE 2012 (2012)","DOI":"10.1145\/2393596.2393665"},{"key":"3_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"715","DOI":"10.1007\/978-3-642-02658-4_60","volume-title":"Computer Aided Verification","author":"C.M. Wintersteiger","year":"2009","unstructured":"Wintersteiger, C.M., Hamadi, Y., de Moura, L.: A concurrent portfolio approach to SMT solving. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol.\u00a05643, pp. 715\u2013720. Springer, Heidelberg (2009)"},{"issue":"1","key":"3_CR24","doi-asserted-by":"crossref","first-page":"565","DOI":"10.1613\/jair.2490","volume":"32","author":"L. Xu","year":"2008","unstructured":"Xu, L., Hutter, F., Hoos, H.H., Leyton-Brown, K.: SATzilla: portfolio-based algorithm selection for SAT. JAIR\u00a032(1), 565\u2013606 (2008)","journal-title":"JAIR"},{"key":"3_CR25","doi-asserted-by":"crossref","unstructured":"Yang, G., P\u0103s\u0103reanu, C.S., Khurshid, S.: Memoized symbolic execution. In: ISSTA 2012 (2012)","DOI":"10.1145\/2338965.2336771"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-39799-8_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,15]],"date-time":"2019-05-15T14:38:28Z","timestamp":1557931108000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-39799-8_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642397981","9783642397998"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-39799-8_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013]]}}}