{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T21:05:38Z","timestamp":1776373538455,"version":"3.51.2"},"publisher-location":"Cham","reference-count":155,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319105741","type":"print"},{"value":"9783319105758","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"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":[[2018]]},"DOI":"10.1007\/978-3-319-10575-8_19","type":"book-chapter","created":{"date-parts":[[2018,5,18]],"date-time":"2018-05-18T04:05:28Z","timestamp":1526616328000},"page":"613-649","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":23,"title":["Combining Model Checking and Testing"],"prefix":"10.1007","author":[{"given":"Patrice","family":"Godefroid","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Koushik","family":"Sen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,5,19]]},"reference":[{"key":"19_CR1","series-title":"LNCS","first-page":"367","volume-title":"Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"S. Anand","year":"2008","unstructured":"Anand, S., Godefroid, P., Tillmann, N.: Demand-driven compositional symbolic execution. In: Ramakrishnan, C.R., Rehof, J. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol.\u00a04963, pp.\u00a0367\u2013381. Springer, Heidelberg (2008)"},{"key":"19_CR2","series-title":"LNCS","first-page":"134","volume-title":"Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"S. Anand","year":"2007","unstructured":"Anand, S., P\u0103s\u0103reanu, C.S., Visser, W.: JPF-SE: a symbolic execution extension to Java PathFinder. In: Grumberg, O., Huth, M. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol.\u00a04424, pp.\u00a0134\u2013138. Springer, Heidelberg (2007)"},{"issue":"4","key":"19_CR3","doi-asserted-by":"crossref","first-page":"474","DOI":"10.1109\/TSE.2010.31","volume":"36","author":"S. Artzi","year":"2010","unstructured":"Artzi, S., Kiezun, A., Dolby, J., Tip, F., Dig, D., Paradkar, A.M., Ernst, M.D.: Finding bugs in web applications using dynamic test generation and explicit-state model checking. IEEE Trans. Softw. Eng. 36(4), 474\u2013494 (2010)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"19_CR4","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"260","DOI":"10.1007\/3-540-44585-4_25","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"T. Ball","year":"2001","unstructured":"Ball, T., Rajamani, S.K.: The SLAM toolkit. In: Berry, G., Comon, H., Finkel, A. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a02102, pp.\u00a0260\u2013264. Springer, Heidelberg (2001)"},{"key":"19_CR5","series-title":"LNCS","first-page":"364","volume-title":"Formal Methods for Components and Objects (FMCO)","author":"M. Barnett","year":"2005","unstructured":"Barnett, M., Chang, B.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: a modular reusable verifier for object-oriented programs. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.P. (eds.) Formal Methods for Components and Objects (FMCO). LNCS, vol.\u00a04111, pp.\u00a0364\u2013387. Springer, Heidelberg (2005)"},{"key":"19_CR6","first-page":"3","volume-title":"Intl. Symp. on Software Testing and Analysis (ISSTA)","author":"N.E. Beckman","year":"2008","unstructured":"Beckman, N.E., Nori, A.V., Rajamani, S.K., Simmons, R.J.: Proofs from tests. In: Ryder, B.G., Zeller, A. (eds.) Intl. Symp. on Software Testing and Analysis (ISSTA), pp.\u00a03\u201314. ACM, New York (2008)"},{"key":"19_CR7","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1007\/11589976_2","volume-title":"Integrated Formal Methods (IFM)","author":"S. Bensalem","year":"2005","unstructured":"Bensalem, S., Peled, D., Qu, H., Tripakis, S.: Generating path conditions for timed systems. In: Romijn, J., Smith, G., van de Pol, J. (eds.) Integrated Formal Methods (IFM). LNCS, vol.\u00a03771, pp.\u00a05\u201319. Springer, Heidelberg (2005)"},{"key":"19_CR8","series-title":"LNCS","first-page":"120","volume-title":"Intl. Haifa Verification Conf. (HVC)","author":"S. Bensalem","year":"2007","unstructured":"Bensalem, S., Peled, D., Qu, H., Tripakis, S., Zuck, L.D.: Test case generation for ultimately periodic paths. In: Yorav, K. (ed.) Intl. Haifa Verification Conf. (HVC). LNCS, vol.\u00a04899, pp.\u00a0120\u2013135. Springer, Heidelberg (2007)"},{"key":"19_CR9","first-page":"326","volume-title":"Intl. Conf. on Software Engineering (ICSE)","author":"D. Beyer","year":"2004","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.) Intl. Conf. on Software Engineering (ICSE), pp.\u00a0326\u2013335. IEEE, Piscataway (2004)"},{"key":"19_CR10","first-page":"57","volume-title":"Intl. Symp. on Foundations of Software Engineering (FSE)","author":"D. Beyer","year":"2012","unstructured":"Beyer, D., Henzinger, T.A., Keremoglu, M.E., Wendler, P.: Conditional model checking: a\u00a0technique to pass information between verifiers. In: Tracz, W., Robillard, M.P., Bultan, T. (eds.) Intl. Symp. on Foundations of Software Engineering (FSE), p.\u00a057. ACM, New York (2012)"},{"key":"19_CR11","first-page":"29","volume-title":"Intl. Conf. on Automated Software Engineering (ASE)","author":"D. Beyer","year":"2008","unstructured":"Beyer, D., Henzinger, T.A., Th\u00e9oduloz, G.: Program analysis with dynamic precision adjustment. In: Intl. Conf. on Automated Software Engineering (ASE), pp.\u00a029\u201338. IEEE, Piscataway (2008)"},{"key":"19_CR12","series-title":"LNCS","first-page":"472","volume-title":"European Symp. on Programming (ESOP)","author":"D. Beyer","year":"2013","unstructured":"Beyer, D., Holzer, A., Tautschnig, M., Veith, H.: Information reuse for multi-goal reachability analyses. In: Felleisen, M., Gardner, P. (eds.) European Symp. on Programming (ESOP). LNCS, vol.\u00a07792, pp.\u00a0472\u2013491. Springer, Heidelberg (2013)"},{"key":"19_CR13","series-title":"LNCS","first-page":"86","volume-title":"Intl. Workshop on Formal Approaches to Testing of Software (FATES)","author":"M. Bijl van der","year":"2003","unstructured":"van der Bijl, M., Rensink, A., Tretmans, J.: Compositional testing with ioco. In: Intl. Workshop on Formal Approaches to Testing of Software (FATES). LNCS, vol.\u00a02931, pp.\u00a086\u2013100. Springer, Heidelberg (2003)"},{"key":"19_CR14","series-title":"LNCS","first-page":"351","volume-title":"Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"P. Boonstoppel","year":"2008","unstructured":"Boonstoppel, P., Cadar, C., Engler, D.R.: Rwset: attacking path explosion in constraint-based test generation. In: Ramakrishnan, C.R., Rehof, J. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol.\u00a04963, pp.\u00a0351\u2013366. Springer, Heidelberg (2008)"},{"key":"19_CR15","first-page":"122","volume-title":"Intl. Conf. on Software Engineering (ICSE)","author":"E. Bounimova","year":"2013","unstructured":"Bounimova, E., Godefroid, P., Molnar, D.A.: Billions and billions of constraints: whitebox fuzz testing in production. In: Notkin, D., Cheng, B.H.C., Pohl, K. (eds.) Intl. Conf. on Software Engineering (ICSE), pp.\u00a0122\u2013131. IEEE\/ACM, Piscataway\/New York (2013)"},{"issue":"6","key":"19_CR16","doi-asserted-by":"crossref","first-page":"234","DOI":"10.1145\/390016.808445","volume":"10","author":"R.S. Boyer","year":"1975","unstructured":"Boyer, R.S., Elspas, B., Levitt, K.N.: SELECT\u2014a formal system for testing and debugging programs by symbolic execution. ACM SIGPLAN Not. 10(6), 234\u2013245 (1975)","journal-title":"ACM SIGPLAN Not."},{"issue":"2\u20133","key":"19_CR17","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1023\/B:FORM.0000040027.28662.a4","volume":"25","author":"G.P. Brat","year":"2004","unstructured":"Brat, G.P., Drusinsky, D., Giannakopoulou, D., Goldberg, A., Havelund, K., Lowry, M.R., P\u0103s\u0103reanu, C.S., Venet, A., Visser, W., Washington, R.: Experimental evaluation of verification and validation tools on Martian Rover software. Form. Methods Syst. Des. 25(2\u20133), 167\u2013198 (2004)","journal-title":"Form. Methods Syst. Des."},{"key":"19_CR18","first-page":"428","volume-title":"Symp. on Logic in Computer Science (LICS)","author":"J.R. Burch","year":"1990","unstructured":"Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 1020$10^{20}$ states and beyond. In: Symp. on Logic in Computer Science (LICS), pp.\u00a0428\u2013439. IEEE, Piscataway (1990)"},{"key":"19_CR19","first-page":"167","volume-title":"Intl. Conf. on Architectural Support for Programming Languages and Operating Systems (ASPLOS)","author":"S. Burckhardt","year":"2010","unstructured":"Burckhardt, S., Kothari, P., Musuvathi, M., Nagarakatte, S.: A randomized scheduler with probabilistic guarantees of finding bugs. In: Hoe, J.C., Adve, V.S. (eds.) Intl. Conf. on Architectural Support for Programming Languages and Operating Systems (ASPLOS), pp.\u00a0167\u2013178. ACM, New York (2010)"},{"key":"19_CR20","first-page":"161","volume-title":"Intl. Conf. on Automated Software Engineering (ASE)","author":"J. Burnim","year":"2009","unstructured":"Burnim, J., Jalbert, N., Stergiou, C., Sen, K.: Looper: lightweight detection of infinite loops at runtime. In: Intl. Conf. on Automated Software Engineering (ASE), pp.\u00a0161\u2013169. IEEE, Piscataway (2009)"},{"key":"19_CR21","first-page":"463","volume-title":"Intl. Conf. on Software Engineering (ICSE)","author":"J. Burnim","year":"2009","unstructured":"Burnim, J., Juvekar, S., Sen, K.: WISE: automated test generation for worst-case complexity. In: Intl. Conf. on Software Engineering (ICSE), pp.\u00a0463\u2013473. IEEE, Piscataway (2009)"},{"key":"19_CR22","volume-title":"USENIX Workshop on Hot Topics in Parallelism (HotPar)","author":"J. Burnim","year":"2010","unstructured":"Burnim, J., Necula, G., Sen, K.: Separating functional and parallel correctness using nondeterministic sequential specifications. In: USENIX Workshop on Hot Topics in Parallelism (HotPar). USENIX Association, Berkeley (2010)"},{"key":"19_CR23","first-page":"79","volume-title":"Intl. Conf. on Architectural Support for Programming Languages and Operating Systems (ASPLOS)","author":"J. Burnim","year":"2011","unstructured":"Burnim, J., Necula, G.C., Sen, K.: Specifying and checking semantic atomicity for multithreaded programs. In: Gupta, R., Mowry, T.C. (eds.) Intl. Conf. on Architectural Support for Programming Languages and Operating Systems (ASPLOS), pp.\u00a079\u201390. ACM, New York (2011)"},{"key":"19_CR24","first-page":"443","volume-title":"Intl. Conf. on Automated Software Engineering (ASE)","author":"J. Burnim","year":"2008","unstructured":"Burnim, J., Sen, K.: Heuristics for scalable dynamic test generation. In: Intl. Conf. on Automated Software Engineering (ASE), pp.\u00a0443\u2013446. IEEE, Piscataway (2008)"},{"issue":"6","key":"19_CR25","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1145\/1743546.1743572","volume":"53","author":"J. Burnim","year":"2010","unstructured":"Burnim, J., Sen, K.: Asserting and checking determinism for multithreaded programs. Commun. ACM 53(6), 97\u2013105 (2010)","journal-title":"Commun. ACM"},{"key":"19_CR26","series-title":"LNCS","first-page":"11","volume-title":"Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"J. Burnim","year":"2011","unstructured":"Burnim, J., Sen, K., Stergiou, C.: Sound and complete monitoring of sequential consistency for relaxed memory models. In: Abdulla, P.A., Leino, K.R.M. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol.\u00a06605, pp.\u00a011\u201325. Springer, Heidelberg (2011)"},{"key":"19_CR27","first-page":"122","volume-title":"Intl. Symp. on Software Testing and Analysis (ISSTA)","author":"J. Burnim","year":"2011","unstructured":"Burnim, J., Sen, K., Stergiou, C.: Testing concurrent programs on relaxed memory models. In: Dwyer, M.B., Tip, F. (eds.) Intl. Symp. on Software Testing and Analysis (ISSTA), pp.\u00a0122\u2013132. ACM, New York (2011)"},{"key":"19_CR28","first-page":"209","volume-title":"Operating Systems Design and Implementation (OSDI)","author":"C. Cadar","year":"2008","unstructured":"Cadar, C., Dunbar, D., Engler, D.R.: KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. In: Draves, R., van Renesse, R. (eds.) Operating Systems Design and Implementation (OSDI), pp.\u00a0209\u2013224. USENIX Association, Berkeley (2008)"},{"key":"19_CR29","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1007\/11537328_2","volume-title":"Intl. Symp. on Model Checking of Software (SPIN)","author":"C. Cadar","year":"2005","unstructured":"Cadar, C., Engler, D.R.: Execution generated test cases: how to make systems code crash itself. In: Godefroid, P. (ed.) Intl. Symp. on Model Checking of Software (SPIN). LNCS, vol.\u00a03639, pp.\u00a02\u201323. Springer, Heidelberg (2005)"},{"key":"19_CR30","first-page":"322","volume-title":"ACM Conf. on Computer and Communications Security (CCS)","author":"C. Cadar","year":"2006","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 Conf. on Computer and Communications Security (CCS), pp.\u00a0322\u2013335. ACM, New York (2006)"},{"key":"19_CR31","first-page":"1066","volume-title":"Intl. Conf. on Software Engineering (ICSE)","author":"C. Cadar","year":"2011","unstructured":"Cadar, C., Godefroid, P., Khurshid, S., P\u0103s\u0103reanu, C.S., Sen, K., Tillmann, N., Visser, W.: Symbolic execution for software testing in practice: preliminary assessment. In: Taylor, R.N., Gall, H.C., Medvidovic, N. (eds.) Intl. Conf. on Software Engineering (ICSE), pp.\u00a01066\u20131071. ACM, New York (2011)"},{"issue":"2","key":"19_CR32","doi-asserted-by":"crossref","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 56(2), 82\u201390 (2013)","journal-title":"Commun. ACM"},{"key":"19_CR33","first-page":"363","volume-title":"Conf. on Programming Language Design and Implementation (PLDI)","author":"S. Chandra","year":"2009","unstructured":"Chandra, S., Fink, S.J., Sridharan, M.: Snugglebug: a powerful approach to weakest preconditions. In: Hind, M., Diwan, A. (eds.) Conf. on Programming Language Design and Implementation (PLDI), pp.\u00a0363\u2013374. ACM, New York (2009)"},{"key":"19_CR34","first-page":"431","volume-title":"Intl. Conf. on Software Engineering (ICSE)","author":"S. Chandra","year":"2002","unstructured":"Chandra, S., Godefroid, P., Palm, C.: Software model checking in practice: an industrial case study. In: Tracz, W., Young, M., Magee, J. (eds.) Intl. Conf. on Software Engineering (ICSE), pp.\u00a0431\u2013441. ACM, New York (2002)"},{"key":"19_CR35","first-page":"62","volume-title":"Intl. Symp. on Software Testing and Analysis (ISSTA)","author":"J. Chang","year":"1996","unstructured":"Chang, J., Richardson, D.J., Sankar, S.: Structural specification-based testing with ADL. In: Intl. Symp. on Software Testing and Analysis (ISSTA), pp.\u00a062\u201370. ACM, New York (1996)"},{"key":"19_CR36","first-page":"265","volume-title":"Intl. Conf. on Architectural Support for Programming Languages and Operating Systems (ASPLOS)","author":"V. Chipounov","year":"2011","unstructured":"Chipounov, V., Kuznetsov, V., Candea, G.: S2E: a platform for in-vivo multi-path analysis of software systems. In: Gupta, R., Mowry, T.C. (eds.) Intl. Conf. on Architectural Support for Programming Languages and Operating Systems (ASPLOS), pp.\u00a0265\u2013278. ACM, New York (2011)"},{"issue":"1","key":"19_CR37","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1023\/A:1011276507260","volume":"19","author":"E.M. Clarke","year":"2001","unstructured":"Clarke, E.M., Biere, A., Raimi, R., Zhu, Y.: Bounded model checking using satisfiability solving. Form. Methods Syst. Des. 19(1), 7\u201334 (2001)","journal-title":"Form. Methods Syst. Des."},{"key":"19_CR38","series-title":"LNCS","first-page":"52","volume-title":"Workshop on Logics of Programs","author":"E.M. Clarke","year":"1981","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Kozen, D. (ed.) Workshop on Logics of Programs. LNCS, vol.\u00a0131, pp.\u00a052\u201371. Springer, Heidelberg (1981)"},{"issue":"2","key":"19_CR39","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E.M. Clarke","year":"1986","unstructured":"Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. Program. Lang. Syst. 8(2), 244\u2013263 (1986)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"19_CR40","first-page":"368","volume-title":"Design Automation Conf. (DAC)","author":"E.M. Clarke","year":"2003","unstructured":"Clarke, E.M., Kroening, D., Yorav, K.: Behavioral consistency of C and Verilog programs using bounded model checking. In: Design Automation Conf. (DAC), pp.\u00a0368\u2013371. ACM, New York (2003)"},{"key":"19_CR41","doi-asserted-by":"crossref","first-page":"488","DOI":"10.1145\/800191.805647","volume-title":"ACM","author":"L.A. Clarke","year":"1976","unstructured":"Clarke, L.A.: A program testing system. In: ACM, vol.\u00a0176, pp.\u00a0488\u2013491 (1976)"},{"issue":"1","key":"19_CR42","doi-asserted-by":"crossref","first-page":"15","DOI":"10.1016\/0164-1212(85)90004-4","volume":"5","author":"L.A. Clarke","year":"1985","unstructured":"Clarke, L.A., Richardson, D.J.: Applications of symbolic evaluation. J. Syst. Softw. 5(1), 15\u201335 (1985)","journal-title":"J. Syst. Softw."},{"key":"19_CR43","first-page":"202","volume-title":"Symposium on Partial Evaluation and Semantics-Based Program Manipulation","author":"C. Colby","year":"1995","unstructured":"Colby, C.: Analyzing the communication topology of concurrent programs. In: Jones, N.D. (ed.) Symposium on Partial Evaluation and Semantics-Based Program Manipulation, pp.\u00a0202\u2013213. ACM, New York (1995)"},{"key":"19_CR44","first-page":"250","volume-title":"Intl. Symp. on Software Testing and Analysis (ISSTA)","author":"J.C. Corbett","year":"1996","unstructured":"Corbett, J.C.: Constructing abstract models of concurrent real-time software. In: Intl. Symp. on Software Testing and Analysis (ISSTA), pp.\u00a0250\u2013260 (1996)"},{"key":"19_CR45","first-page":"439","volume-title":"Intl. Conf. on Software Engineering (ICSE)","author":"J.C. Corbett","year":"2000","unstructured":"Corbett, J.C., Dwyer, M.B., Hatcliff, J., Laubach, S., P\u0103s\u0103reanu, C.S., Robby, Zheng, H.: Bandera: extracting finite-state models from Java source code. In: Ghezzi, C., Jazayeri, M., Wolf, A.L. (eds.) Intl. Conf. on Software Engineering (ICSE), pp.\u00a0439\u2013448. ACM, New York (2000)"},{"key":"19_CR46","first-page":"214","volume-title":"Symposium on Partial Evaluation and Semantics-Based Program Manipulation","author":"R. Cridlig","year":"1995","unstructured":"Cridlig, R.: Semantic analysis of shared-memory concurrent languages using abstract model-checking. In: Jones, N.D. (ed.) Symposium on Partial Evaluation and Semantics-Based Program Manipulation, pp.\u00a0214\u2013225. ACM, New York (1995)"},{"key":"19_CR47","first-page":"422","volume-title":"Intl. Conf. on Software Engineering (ICSE)","author":"C. Csallner","year":"2005","unstructured":"Csallner, C., Smaragdakis, Y.: Check\u2019n\u2019crash: combining static checking and testing. In: Roman, G., Griswold, W.G., Nuseibeh, B. (eds.) Intl. Conf. on Software Engineering (ICSE), pp.\u00a0422\u2013431. ACM, New York (2005)"},{"issue":"8","key":"19_CR48","doi-asserted-by":"crossref","first-page":"453","DOI":"10.1145\/360933.360975","volume":"18","author":"E.W. Dijkstra","year":"1975","unstructured":"Dijkstra, E.W.: Guarded commands, nondeterminacy and formal derivation of programs. Commun. ACM 18(8), 453\u2013457 (1975)","journal-title":"Commun. ACM"},{"key":"19_CR49","first-page":"140","volume-title":"Intl. Symp. on Foundations of Software Engineering (FSE)","author":"L.K. Dillon","year":"1994","unstructured":"Dillon, L.K., Yu, Q.: Oracles for checking temporal properties of concurrent systems. In: Wile, D.S. (ed.) Intl. Symp. on Foundations of Software Engineering (FSE), pp.\u00a0140\u2013153. ACM, New York (1994)"},{"key":"19_CR50","series-title":"LNCS","first-page":"323","volume-title":"Intl. Symp. on Model Checking of Software (SPIN)","author":"D. Drusinsky","year":"2000","unstructured":"Drusinsky, D.: The temporal rover and the ATG rover. In: Havelund, K., Penix, J., Visser, W. (eds.) Intl. Symp. on Model Checking of Software (SPIN). LNCS, vol.\u00a01885, pp.\u00a0323\u2013330. Springer, Heidelberg (2000)"},{"issue":"3\u20135","key":"19_CR51","doi-asserted-by":"crossref","first-page":"485","DOI":"10.1002\/cpe.654","volume":"15","author":"O. Edelstein","year":"2003","unstructured":"Edelstein, O., Farchi, E., Goldin, E., Nir, Y., Ratsaby, G., Ur, S.: Framework for testing multi-threaded Java programs. Concurr. Comput. 15(3\u20135), 485\u2013499 (2003)","journal-title":"Concurr. Comput."},{"key":"19_CR52","first-page":"129","volume-title":"Intl. Symp. on Software Testing and Analysis (ISSTA)","author":"B. Elkarablieh","year":"2009","unstructured":"Elkarablieh, B., Godefroid, P., Levin, M.Y.: Precise pointer reasoning for dynamic test generation. In: Rothermel, G., Dillon, L.K. (eds.) Intl. Symp. on Software Testing and Analysis (ISSTA), pp.\u00a0129\u2013140. ACM, New York (2009)"},{"key":"19_CR53","first-page":"151","volume-title":"Intl. Symp. on Software Testing and Analysis (ISSTA)","author":"M. Emmi","year":"2007","unstructured":"Emmi, M., Majumdar, R., Sen, K.: Dynamic test input generation for database applications. In: Rosenblum, D.S., Elbaum, S.G. (eds.) Intl. Symp. on Software Testing and Analysis (ISSTA), pp.\u00a0151\u2013162. ACM, New York (2007)"},{"key":"19_CR54","first-page":"25","volume-title":"ICSE Workshop on Dynamic Analysis (WODA)","author":"M.D. Ernst","year":"2003","unstructured":"Ernst, M.D.: Static and dynamic analysis: synergy and duality. In: ICSE Workshop on Dynamic Analysis (WODA), pp.\u00a025\u201328. ACM, New York (2003)"},{"key":"19_CR55","first-page":"37","volume-title":"Intl. Symp. on Foundations of Software Engineering (FSE)","author":"A. Farzan","year":"2013","unstructured":"Farzan, A., Holzer, A., Razavi, N., Veith, H.: Con2colic testing. In: Meyer, B., Baresi, L., Mezini, M. (eds.) Intl. Symp. on Foundations of Software Engineering (FSE), pp.\u00a037\u201347. ACM, New York (2013)"},{"key":"19_CR56","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"348","DOI":"10.1007\/3-540-61474-5_82","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"J. Fernandez","year":"1996","unstructured":"Fernandez, J., Jard, C., J\u00e9ron, T., Viho, C.: Using on-the-fly verification techniques for the generation of test suites. In: Alur, R., Henzinger, T.A. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a01102, pp.\u00a0348\u2013359. Springer, Heidelberg (1996)"},{"key":"19_CR57","first-page":"110","volume-title":"Symp. on Principles of Programming Languages (POPL)","author":"C. Flanagan","year":"2005","unstructured":"Flanagan, C., Godefroid, P.: Dynamic partial-order reduction for model checking software. In: Palsberg, J., Abadi, M. (eds.) Symp. on Principles of Programming Languages (POPL), pp.\u00a0110\u2013121. ACM, New York (2005)"},{"key":"19_CR58","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1090\/psapm\/019\/0235771","volume-title":"Mathematical Aspects of Computer Science","author":"R.W. Floyd","year":"1967","unstructured":"Floyd, R.W.: Assigning meanings to programs. In: Mathematical Aspects of Computer Science, vol.\u00a019, pp.\u00a019\u201332 (1967)"},{"key":"19_CR59","series-title":"LNCS","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-60761-7","volume-title":"Partial-Order Methods for the Verification of Concurrent Systems\u2014An Approach to the State-Explosion Problem","author":"P. Godefroid","year":"1996","unstructured":"Godefroid, P.: Partial-Order Methods for the Verification of Concurrent Systems\u2014An Approach to the State-Explosion Problem. LNCS, vol.\u00a01032. Springer, Heidelberg (1996)"},{"key":"19_CR60","first-page":"174","volume-title":"Symp. on Principles of Programming Languages (POPL)","author":"P. Godefroid","year":"1997","unstructured":"Godefroid, P.: Model checking for programming languages using VeriSoft. In: Lee, P., Henglein, F., Jones, N.D. (eds.) Symp. on Principles of Programming Languages (POPL), pp.\u00a0174\u2013186. ACM, New York (1997)"},{"issue":"2","key":"19_CR61","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1007\/s10703-005-1489-x","volume":"26","author":"P. Godefroid","year":"2005","unstructured":"Godefroid, P.: Software model checking: the VeriSoft approach. Form. Methods Syst. Des. 26(2), 77\u2013101 (2005)","journal-title":"Form. Methods Syst. Des."},{"key":"19_CR62","first-page":"47","volume-title":"Symp. on Principles of Programming Languages (POPL)","author":"P. Godefroid","year":"2007","unstructured":"Godefroid, P.: Compositional dynamic test generation. In: Hofmann, M., Felleisen, M. (eds.) Symp. on Principles of Programming Languages (POPL), pp.\u00a047\u201354. ACM, New York (2007)"},{"key":"19_CR63","first-page":"258","volume-title":"Conf. on Programming Language Design and Implementation (PLDI)","author":"P. Godefroid","year":"2011","unstructured":"Godefroid, P.: Higher-order test generation. In: Hall, M.W., Padua, D.A. (eds.) Conf. on Programming Language Design and Implementation (PLDI), pp.\u00a0258\u2013269. ACM, New York (2011)"},{"key":"19_CR64","first-page":"124","volume-title":"Intl. Symp. on Software Testing and Analysis (ISSTA)","author":"P. Godefroid","year":"1998","unstructured":"Godefroid, P., Hanmer, R.S., Jagadeesan, L.J.: Model checking without a model: an analysis of the heart-beat monitor of a telephone switch using VeriSoft. In: Intl. Symp. on Software Testing and Analysis (ISSTA), pp.\u00a0124\u2013133 (1998)"},{"key":"19_CR65","series-title":"LNCS","first-page":"426","volume-title":"Intl. Conf. on Concurrency Theory (CONCUR)","author":"P. Godefroid","year":"2001","unstructured":"Godefroid, P., Huth, M., Jagadeesan, R.: Abstraction-based model checking using modal transition systems. In: Larsen, K.G., Nielsen, M. (eds.) Intl. Conf. on Concurrency Theory (CONCUR). LNCS, vol.\u00a02154, pp.\u00a0426\u2013440. Springer, Heidelberg (2001)"},{"key":"19_CR66","first-page":"206","volume-title":"Conf. on Programming Language Design and Implementation (PLDI)","author":"P. Godefroid","year":"2008","unstructured":"Godefroid, P., Kiezun, A., Levin, M.Y.: Grammar-based whitebox fuzzing. In: Conf. on Programming Language Design and Implementation (PLDI), pp.\u00a0206\u2013215. ACM, New York (2008)"},{"key":"19_CR67","first-page":"1","volume-title":"Intl. Symp. on Software Testing and Analysis (ISSTA)","author":"P. Godefroid","year":"2010","unstructured":"Godefroid, P., Kinder, J.: Proving memory safety of floating-point computations by combining static and dynamic program analysis. In: Tonella, P., Orso, A. (eds.) Intl. Symp. on Software Testing and Analysis (ISSTA), pp.\u00a01\u201312. ACM, New York (2010)"},{"key":"19_CR68","first-page":"213","volume-title":"Conf. on Programming Language Design and Implementation (PLDI)","author":"P. Godefroid","year":"2005","unstructured":"Godefroid, P., Klarlund, N., Sen, K.: DART: Directed Automated Random Testing. In: Sarkar, V., Hall, M.W. (eds.) Conf. on Programming Language Design and Implementation (PLDI), pp.\u00a0213\u2013223. ACM, New York (2005)"},{"key":"19_CR69","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1007\/978-3-642-35746-6_2","volume-title":"Tools for Practical Software Verification (LASER)","author":"P. Godefroid","year":"2012","unstructured":"Godefroid, P., Lahiri, S.K.: From program to logic: an introduction. In: Meyer, B., Nordio, M. (eds.) Tools for Practical Software Verification (LASER). LNCS, vol.\u00a07682, pp.\u00a031\u201344. Springer, Heidelberg (2012)"},{"key":"19_CR70","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"112","DOI":"10.1007\/978-3-642-23702-7_12","volume-title":"Intl. Symp. on Static Analysis (SAS)","author":"P. Godefroid","year":"2011","unstructured":"Godefroid, P., Lahiri, S.K., Rubio-Gonz\u00e1lez, C.: Statically validating must summaries for incremental compositional dynamic test generation. In: Yahav, E. (ed.) Intl. Symp. on Static Analysis (SAS). LNCS, vol.\u00a06887, pp.\u00a0112\u2013128. Springer, Heidelberg (2011)"},{"key":"19_CR71","first-page":"207","volume-title":"Intl. Conf. on Embedded Software (EMSOFT)","author":"P. Godefroid","year":"2008","unstructured":"Godefroid, P., Levin, M.Y., Molnar, D.A.: Active property checking. In: de Alfaro, L., Palsberg, J. (eds.) Intl. Conf. on Embedded Software (EMSOFT), pp.\u00a0207\u2013216. ACM, New York (2008)"},{"key":"19_CR72","volume-title":"Network and Distributed System Security Symposium (NDSS)","author":"P. Godefroid","year":"2008","unstructured":"Godefroid, P., Levin, M.Y., Molnar, D.A.: Automated whitebox fuzz testing. In: Network and Distributed System Security Symposium (NDSS). The Internet Society, Reston (2008)"},{"issue":"3","key":"19_CR73","doi-asserted-by":"crossref","first-page":"40","DOI":"10.1145\/2093548.2093564","volume":"55","author":"P. Godefroid","year":"2012","unstructured":"Godefroid, P., Levin, M.Y., Molnar, D.A.: SAGE: whitebox fuzzing for security testing. Commun. ACM 55(3), 40\u201344 (2012)","journal-title":"Commun. ACM"},{"key":"19_CR74","first-page":"23","volume-title":"Intl. Symp. on Software Testing and Analysis (ISSTA)","author":"P. Godefroid","year":"2011","unstructured":"Godefroid, P., Luchaup, D.: Automatic partial loop summarization in dynamic test generation. In: Dwyer, M.B., Tip, F. (eds.) Intl. Symp. on Software Testing and Analysis (ISSTA), pp.\u00a023\u201333. ACM, New York (2011)"},{"key":"19_CR75","first-page":"43","volume-title":"Symp. on Principles of Programming Languages (POPL)","author":"P. Godefroid","year":"2010","unstructured":"Godefroid, P., Nori, A.V., Rajamani, S.K., Tetali, S.: Compositional may-must program analysis: unleashing the power of alternation. In: Hermenegildo, M.V., Palsberg, J. (eds.) Symp. on Principles of Programming Languages (POPL), pp.\u00a043\u201356. ACM, New York (2010)"},{"key":"19_CR76","first-page":"441","volume-title":"Conf. on Programming Language Design and Implementation (PLDI)","author":"P. Godefroid","year":"2012","unstructured":"Godefroid, P., Taly, A.: Automated synthesis of symbolic instruction encodings from I\/O samples. In: Vitek, J., Lin, H., Tip, F. (eds.) Conf. on Programming Language Design and Implementation (PLDI), pp.\u00a0441\u2013452. ACM, New York (2012)"},{"key":"19_CR77","first-page":"117","volume-title":"Intl. Symp. on Foundations of Software Engineering (FSE)","author":"B.S. Gulavani","year":"2006","unstructured":"Gulavani, B.S., Henzinger, T.A., Kannan, Y., Nori, A.V., Rajamani, S.K.: SYNERGY: a new algorithm for property checking. In: Young, M., Devanbu, P.T. (eds.) Intl. Symp. on Foundations of Software Engineering (FSE), pp.\u00a0117\u2013127. ACM, New York (2006)"},{"key":"19_CR78","series-title":"LNCS","first-page":"405","volume-title":"Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"E.L. Gunter","year":"1999","unstructured":"Gunter, E.L., Peled, D.: Path exploration tool. In: Cleaveland, R. (ed.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol.\u00a01579, pp.\u00a0405\u2013419. Springer, Heidelberg (1999)"},{"issue":"2","key":"19_CR79","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1007\/s00165-005-0059-8","volume":"17","author":"E.L. Gunter","year":"2005","unstructured":"Gunter, E.L., Peled, D.: Model checking, testing and verification working together. Form. Asp. Comput. 17(2), 201\u2013221 (2005)","journal-title":"Form. Asp. Comput."},{"key":"19_CR80","first-page":"219","volume-title":"Intl. Conf. on Automated Software Engineering (ASE)","author":"N. Gupta","year":"2000","unstructured":"Gupta, N., Mathur, A.P., Soffa, M.L.: Generating test data for branch coverage. In: Intl. Conf. on Automated Software Engineering (ASE), pp.\u00a0219\u2013228. IEEE, Piscataway (2000)"},{"issue":"2","key":"19_CR81","doi-asserted-by":"crossref","first-page":"200","DOI":"10.1016\/S1571-0661(04)00253-1","volume":"55","author":"K. Havelund","year":"2001","unstructured":"Havelund, K., Rosu, G.: Monitoring Java programs with Java PathExplorer. Electron. Notes Theor. Comput. Sci. 55(2), 200\u2013217 (2001)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"19_CR82","first-page":"171","volume-title":"Formal Methods in Computer Aided Design (FMCAD)","author":"C. Helmstetter","year":"2006","unstructured":"Helmstetter, C., Maraninchi, F., Maillet-Contoz, L., Moy, M.: Automatic generation of schedulings for improving the test coverage of systems-on-a-chip. In: Formal Methods in Computer Aided Design (FMCAD), pp.\u00a0171\u2013178. IEEE, Piscataway (2006)"},{"issue":"10","key":"19_CR83","doi-asserted-by":"crossref","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C.A.R. Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576\u2013580 (1969)","journal-title":"Commun. ACM"},{"key":"19_CR84","series-title":"LNCS","first-page":"338","volume-title":"World Congress on Formal Methods","author":"J. Hoenicke","year":"2009","unstructured":"Hoenicke, J., Leino, K.R.M., Podelski, A., Sch\u00e4f, M., Wies, T.: It\u2019s doomed; we can prove it. In: Cavalcanti, A., Dams, D. (eds.) World Congress on Formal Methods. LNCS, vol.\u00a05850, pp.\u00a0338\u2013353. Springer, Heidelberg (2009)"},{"key":"19_CR85","first-page":"597","volume-title":"Intl. Conf. on Software Engineering (ICSE)","author":"G.J. Holzmann","year":"1999","unstructured":"Holzmann, G.J., Smith, M.H.: A practical method for verifying event-driven software. In: Boehm, B.W., Garlan, D., Kramer, J. (eds.) Intl. Conf. on Software Engineering (ICSE), pp.\u00a0597\u2013607. ACM, New York (1999)"},{"issue":"4","key":"19_CR86","doi-asserted-by":"crossref","first-page":"266","DOI":"10.1109\/TSE.1977.231144","volume":"3","author":"W.E. Howden","year":"1977","unstructured":"Howden, W.E.: Symbolic testing and the DISSECT symbolic evaluation system. IEEE Trans. Softw. Eng. 3(4), 266\u2013278 (1977)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"19_CR87","first-page":"525","volume-title":"Intl. Conf. on Software Engineering (ICSE)","author":"L.J. Jagadeesan","year":"1997","unstructured":"Jagadeesan, L.J., Porter, A.A., Puchol, C., Ramming, J.C., Votta, L.G.: Specification-based testing of reactive software: tools and experiments (experience report). In: Adrion, W.R., Fuggetta, A., Taylor, R.N., Wasserman, A.I. (eds.) Intl. Conf. on Software Engineering (ICSE), pp.\u00a0525\u2013535. ACM, New York (1997)"},{"key":"19_CR88","first-page":"57","volume-title":"Intl. Symp. on Foundations of Software Engineering (FSE)","author":"N. Jalbert","year":"2010","unstructured":"Jalbert, N., Sen, K.: A trace simplification technique for effective debugging of concurrent programs. In: Roman, G., Sullivan, K.J. (eds.) Intl. Symp. on Foundations of Software Engineering (FSE), pp.\u00a057\u201366. ACM, New York (2010)"},{"key":"19_CR89","doi-asserted-by":"crossref","first-page":"675","DOI":"10.1007\/978-3-642-02658-4_54","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"P. Joshi","year":"2009","unstructured":"Joshi, P., Naik, M., Park, C., Sen, K.: CalFuzzer: an extensible active testing framework for concurrent programs. In: Bouajjani, A., Maler, O. (eds.) Intl. Conf. on Computer-Aided Verification (CAV), pp.\u00a0675\u2013681 (2009)"},{"key":"19_CR90","first-page":"327","volume-title":"Intl. Symp. on Foundations of Software Engineering (FSE)","author":"P. Joshi","year":"2010","unstructured":"Joshi, P., Naik, M., Sen, K., Gay, D.: An effective dynamic analysis for detecting generalized deadlocks. In: Roman, G., Sullivan, K.J. (eds.) Intl. Symp. on Foundations of Software Engineering (FSE), pp.\u00a0327\u2013336. ACM, New York (2010)"},{"key":"19_CR91","first-page":"110","volume-title":"Conf. on Programming Language Design and Implementation (PLDI)","author":"P. Joshi","year":"2009","unstructured":"Joshi, P., Park, C., Sen, K., Naik, M.: A randomized dynamic program analysis technique for detecting real deadlocks. In: Hind, M., Diwan, A. (eds.) Conf. on Programming Language Design and Implementation (PLDI), pp.\u00a0110\u2013120. ACM, New York (2009)"},{"key":"19_CR92","first-page":"561","volume-title":"Intl. Symp. on Foundations of Software Engineering (FSE)","author":"P. Joshi","year":"2007","unstructured":"Joshi, P., Sen, K., Shlimovich, M.: Predictive testing: amplifying the effectiveness of software testing. In: Crnkovic, I., Bertolino, A. (eds.) Intl. Symp. on Foundations of Software Engineering (FSE), pp.\u00a0561\u2013564 (2007)"},{"key":"19_CR93","first-page":"283","volume-title":"Intl. Symp. on Software Testing and Analysis (ISSTA)","author":"Y. Kannan","year":"2008","unstructured":"Kannan, Y., Sen, K.: Universal symbolic execution and its application to likely data structure invariant generation. In: Ryder, B.G., Zeller, A. (eds.) Intl. Symp. on Software Testing and Analysis (ISSTA), pp.\u00a0283\u2013294. ACM, New York (2008)"},{"key":"19_CR94","series-title":"LNCS","first-page":"553","volume-title":"Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","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.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol.\u00a02619, pp.\u00a0553\u2013568. Springer, Heidelberg (2003)"},{"key":"19_CR95","volume-title":"USENIX Symp. on Networked Systems Design and Implementation (NSDI)","author":"C.E. Killian","year":"2007","unstructured":"Killian, C.E., Anderson, J.W., Jhala, R., Vahdat, A.: Life, death, and the critical transition: finding liveness bugs in systems code. In: Balakrishnan, H., Druschel, P. (eds.) USENIX Symp. on Networked Systems Design and Implementation (NSDI). USENIX Association, Berkeley (2007)"},{"issue":"7","key":"19_CR96","doi-asserted-by":"crossref","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 19(7), 385\u2013394 (1976)","journal-title":"Commun. ACM"},{"key":"19_CR97","first-page":"311","volume-title":"IEEE Conference on Software Maintenance","author":"B. Korel","year":"1990","unstructured":"Korel, B.: A dynamic approach of test data generation. In: IEEE Conference on Software Maintenance, pp.\u00a0311\u2013317. IEEE, Piscataway (1990)"},{"key":"19_CR98","volume-title":"USENIX Annual Technical Conference","author":"V. Kuznetsov","year":"2010","unstructured":"Kuznetsov, V., Chipounov, V., Candea, G.: Testing closed-source binary device drivers with DDT. In: Barham, P., Roscoe, T. (eds.) USENIX Annual Technical Conference. USENIX Association, Berkeley (2010)"},{"key":"19_CR99","first-page":"97","volume-title":"Symp. on Principles of Programming Languages (POPL)","author":"O. Lichtenstein","year":"1985","unstructured":"Lichtenstein, O., Pnueli, A.: Checking that finite state concurrent programs satisfy their linear specification. In: Deusen, M.S.V., Galil, Z., Reid, B.K. (eds.) Symp. on Principles of Programming Languages (POPL), pp.\u00a097\u2013107. ACM, New York (1985)"},{"key":"19_CR100","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1145\/120807.120810","volume-title":"Symposium on Testing, Analysis, and Verification","author":"D.L. Long","year":"1991","unstructured":"Long, D.L., Clarke, L.A.: Data flow analysis of concurrent systems that use the rendezvous model of synchronization. In: Symposium on Testing, Analysis, and Verification, pp.\u00a021\u201335 (1991)"},{"key":"19_CR101","doi-asserted-by":"crossref","first-page":"416","DOI":"10.1109\/ICSE.2007.41","volume-title":"Intl. Conf. on Software Engineering (ICSE)","author":"R. Majumdar","year":"2007","unstructured":"Majumdar, R., Sen, K.: Hybrid concolic testing. In: Intl. Conf. on Software Engineering (ICSE), pp.\u00a0416\u2013426. IEEE, Piscataway (2007)"},{"key":"19_CR102","first-page":"134","volume-title":"Intl. Conf. on Automated Software Engineering (ASE)","author":"R. Majumdar","year":"2007","unstructured":"Majumdar, R., Xu, R.: Directed test generation using symbolic grammars. In: Stirewalt, R.E.K., Egyed, A., Fischer, B. (eds.) Intl. Conf. on Automated Software Engineering (ASE), pp.\u00a0134\u2013143. ACM, New York (2007)"},{"key":"19_CR103","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"555","DOI":"10.1007\/978-3-642-02658-4_41","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"R. Majumdar","year":"2009","unstructured":"Majumdar, R., Xu, R.: Reducing test inputs using information partitions. In: Bouajjani, A., Maler, O. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a05643, pp.\u00a0555\u2013569. Springer, Heidelberg (2009)"},{"key":"19_CR104","first-page":"129","volume-title":"Symposium on Principles and Practice of Parallel Programming (PPOPP)","author":"S.P. Masticola","year":"1993","unstructured":"Masticola, S.P., Ryder, B.G.: Non-concurrency analysis. In: Chen, M.C., Halstead, R. (eds.) Symposium on Principles and Practice of Parallel Programming (PPOPP), pp.\u00a0129\u2013138. ACM, New York (1993)"},{"key":"19_CR105","unstructured":"Molnar, D.A., Wagner, D.: CatchConv: symbolic execution and run-time type inference for integer conversion errors. Tech. Rep. UCB\/EECS-2007-23, EECS Department, University of California, Berkeley (2007)"},{"key":"19_CR106","series-title":"LNCS","first-page":"337","volume-title":"Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"L.M. Moura de","year":"2008","unstructured":"de Moura, L.M., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol.\u00a04963, pp.\u00a0337\u2013340. Springer, Heidelberg (2008)"},{"key":"19_CR107","first-page":"155","volume-title":"USENIX Symp. on Networked Systems Design and Implementation (NSDI)","author":"M. Musuvathi","year":"2004","unstructured":"Musuvathi, M., Engler, D.R.: Model checking large network protocol implementations. In: Morris, R., Savage, S. (eds.) USENIX Symp. on Networked Systems Design and Implementation (NSDI), pp.\u00a0155\u2013168. USENIX Association, Berkeley (2004)"},{"key":"19_CR108","first-page":"75","volume-title":"Operating Systems Design and Implementation (OSDI)","author":"M. Musuvathi","year":"2002","unstructured":"Musuvathi, M., Park, D.Y.W., Chou, A., Engler, D.R., Dill, D.L.: CMC: a pragmatic approach to model checking real code. In: Culler, D.E., Druschel, P. (eds.) Operating Systems Design and Implementation (OSDI), pp.\u00a075\u201388. USENIX Association, Berkeley (2002)"},{"key":"19_CR109","first-page":"446","volume-title":"Conf. on Programming Language Design and Implementation (PLDI)","author":"M. Musuvathi","year":"2007","unstructured":"Musuvathi, M., Qadeer, S.: Iterative context bounding for systematic testing of multithreaded programs. In: Ferrante, J., McKinley, K.S. (eds.) Conf. on Programming Language Design and Implementation (PLDI), pp.\u00a0446\u2013455. ACM, New York (2007)"},{"key":"19_CR110","first-page":"267","volume-title":"Operating Systems Design and Implementation (OSDI)","author":"M. Musuvathi","year":"2008","unstructured":"Musuvathi, M., Qadeer, S., Ball, T., Basler, G., Nainar, P.A., Neamtiu, I.: Finding and reproducing heisenbugs in concurrent programs. In: Draves, R., van Renesse, R. (eds.) Operating Systems Design and Implementation (OSDI), pp.\u00a0267\u2013280. USENIX Association, Berkeley (2008)"},{"key":"19_CR111","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"435","DOI":"10.1007\/10722167_33","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"K.S. Namjoshi","year":"2000","unstructured":"Namjoshi, K.S., Kurshan, R.P.: Syntactic program transformations for automatic abstraction. In: Emerson, E.A., Sistla, A.P. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a01855, pp.\u00a0435\u2013449. Springer, Heidelberg (2000)"},{"key":"19_CR112","first-page":"128","volume-title":"Symp. on Principles of Programming Languages (POPL)","author":"G.C. Necula","year":"2002","unstructured":"Necula, G.C., McPeak, S., Weimer, W.: CCured: type-safe retrofitting of legacy code. In: Launchbury, J., Mitchell, J.C. (eds.) Symp. on Principles of Programming Languages (POPL), pp.\u00a0128\u2013139. ACM, New York (2002)"},{"key":"19_CR113","first-page":"355","volume-title":"Intl. Conf. on Software Engineering (ICSE)","author":"A.V. Nori","year":"2010","unstructured":"Nori, A.V., Rajamani, S.K.: An empirical study of optimizations in YOGI. In: Kramer, J., Bishop, J., Devanbu, P.T., Uchitel, S. (eds.) Intl. Conf. on Software Engineering (ICSE), pp.\u00a0355\u2013364. ACM, New York (2010)"},{"issue":"2","key":"19_CR114","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1002\/(SICI)1097-024X(199902)29:2<167::AID-SPE225>3.0.CO;2-V","volume":"29","author":"A.J. Offutt","year":"1999","unstructured":"Offutt, A.J., Jin, Z., Pan, J.: The dynamic domain reduction procedure for test data generation. Softw. Pract. Exp. 29(2), 167\u2013193 (1999)","journal-title":"Softw. Pract. Exp."},{"key":"19_CR115","first-page":"135","volume-title":"Intl. Symp. on Foundations of Software Engineering (FSE)","author":"C. Park","year":"2008","unstructured":"Park, C., Sen, K.: Randomized active atomicity violation detection in concurrent programs. In: Harrold, M.J., Murphy, G.C. (eds.) Intl. Symp. on Foundations of Software Engineering (FSE), pp.\u00a0135\u2013145. ACM, New York (2008)"},{"key":"19_CR116","first-page":"51:1","volume-title":"Conference on High Performance Computing Networking, Storage and Analysis (SC)","author":"C. Park","year":"2011","unstructured":"Park, C., Sen, K., Hargrove, P., Iancu, C.: Efficient data race detection for distributed memory parallel programs. In: Lathrop, S., Costa, J., Kramer, W. (eds.) Conference on High Performance Computing Networking, Storage and Analysis (SC), pp.\u00a051:1\u201351:12. ACM, New York (2011)"},{"key":"19_CR117","first-page":"47","volume-title":"International Conference on Supercomputing (ICS)","author":"C. Park","year":"2013","unstructured":"Park, C., Sen, K., Iancu, C.: Scaling data race detection for partitioned global address space programs. In: Malony, A.D., Nemirovsky, M., Midkiff, S.P. (eds.) International Conference on Supercomputing (ICS), pp.\u00a047\u201358. ACM, New York (2013)"},{"key":"19_CR118","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"409","DOI":"10.1007\/3-540-56922-7_34","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"D. Peled","year":"1993","unstructured":"Peled, D.: All from one, one for all: on model checking using representatives. In: Courcoubetis, C. (ed.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a0697, pp.\u00a0409\u2013423. Springer, Heidelberg (1993)"},{"issue":"2","key":"19_CR119","doi-asserted-by":"crossref","first-page":"103","DOI":"10.1007\/s10703-005-1490-4","volume":"26","author":"J. Penix","year":"2005","unstructured":"Penix, J., Visser, W., Park, S., P\u0103s\u0103reanu, C.S., Engstrom, E., Larson, A., Weininger, N.: Verifying time partitioning in the DEOS scheduling kernel. Form. Methods Syst. Des. 26(2), 103\u2013135 (2005)","journal-title":"Form. Methods Syst. Des."},{"key":"19_CR120","first-page":"226","volume-title":"Intl. Symp. on Foundations of Software Engineering (FSE)","author":"S. Person","year":"2008","unstructured":"Person, S., Dwyer, M.B., Elbaum, S.G., P\u0103s\u0103reanu, C.S.: Differential symbolic execution. In: Harrold, M.J., Murphy, G.C. (eds.) Intl. Symp. on Foundations of Software Engineering (FSE), pp.\u00a0226\u2013237. ACM, New York (2008)"},{"key":"19_CR121","first-page":"504","volume-title":"Conf. on Programming Language Design and Implementation (PLDI)","author":"S. Person","year":"2011","unstructured":"Person, S., Yang, G., Rungta, N., Khurshid, S.: Directed incremental symbolic execution. In: Hall, M.W., Padua, D.A. (eds.) Conf. on Programming Language Design and Implementation (PLDI), pp.\u00a0504\u2013515. ACM, New York (2011)"},{"key":"19_CR122","series-title":"LNCS","first-page":"93","volume-title":"Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"S. Qadeer","year":"2005","unstructured":"Qadeer, S., Rehof, J.: Context-bounded model checking of concurrent software. In: Halbwachs, N., Zuck, L.D. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol.\u00a03440, pp.\u00a093\u2013107. Springer, Heidelberg (2005)"},{"key":"19_CR123","first-page":"14","volume-title":"Conf. on Programming Language Design and Implementation (PLDI)","author":"S. Qadeer","year":"2004","unstructured":"Qadeer, S., Wu, D.: KISS: keep it simple and sequential. In: Pugh, W., Chambers, C. (eds.) Conf. on Programming Language Design and Implementation (PLDI), pp.\u00a014\u201324. ACM, New York (2004)"},{"key":"19_CR124","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1007\/3-540-11494-7_22","volume-title":"International Symposium on Programming","author":"J. Queille","year":"1982","unstructured":"Queille, J., Sifakis, J.: Specification and verification of concurrent systems in CESAR. In: Dezani-Ciancaglini, M., Montanari, U. (eds.) International Symposium on Programming. LNCS, vol.\u00a0137, pp.\u00a0337\u2013351. Springer, Heidelberg (1982)"},{"issue":"4","key":"19_CR125","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1109\/TSE.1976.233835","volume":"2","author":"C.V. Ramamoorthy","year":"1976","unstructured":"Ramamoorthy, C.V., Ho, S.F., Chen, W.T.: On the automated generation of program test data. IEEE Trans. Softw. Eng. 2(4), 293\u2013300 (1976)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"19_CR126","doi-asserted-by":"crossref","first-page":"239","DOI":"10.1007\/978-3-642-35182-2_17","volume-title":"Asian Symp. on Programming Languages and Systems (APLAS)","author":"N. Razavi","year":"2012","unstructured":"Razavi, N., Ivancic, F., Kahlon, V., Gupta, A.: Concurrent test generation using concolic multi-trace analysis. In: Jhala, R., Igarashi, A. (eds.) Asian Symp. on Programming Languages and Systems (APLAS), pp.\u00a0239\u2013255. Springer, Heidelberg (2012)"},{"key":"19_CR127","first-page":"138","volume-title":"Intl. Symp. on Software Testing and Analysis (ISSTA)","author":"D.J. Richardson","year":"1994","unstructured":"Richardson, D.J.: TAOS: testing with analysis and oracle support. In: Intl. Symp. on Software Testing and Analysis (ISSTA), pp.\u00a0138\u2013153 (1994)"},{"key":"19_CR128","first-page":"513","volume-title":"Symposium on Security and Privacy","author":"P. Saxena","year":"2010","unstructured":"Saxena, P., Akhawe, D., Hanna, S., Mao, F., McCamant, S., Song, D.: A symbolic execution framework for JavaScript. In: Symposium on Security and Privacy, pp.\u00a0513\u2013528. IEEE, Piscataway (2010)"},{"key":"19_CR129","first-page":"225","volume-title":"Intl. Symp. on Software Testing and Analysis (ISSTA)","author":"P. Saxena","year":"2009","unstructured":"Saxena, P., Poosankam, P., McCamant, S., Song, D.: Loop-extended symbolic execution on binary programs. In: Rothermel, G., Dillon, L.K. (eds.) Intl. Symp. on Software Testing and Analysis (ISSTA), pp.\u00a0225\u2013236. ACM, New York (2009)"},{"key":"19_CR130","unstructured":"Sen, K.: CATG: a concolic testing tool for sequential Java programs. https:\/\/github.com\/ksen007\/janala2"},{"key":"19_CR131","unstructured":"Sen, K.: Scalable automated methods for dynamic program analysis. Ph.D. thesis, University of Illinois at Urbana-Champaign (2006)"},{"key":"19_CR132","first-page":"323","volume-title":"Intl. Conf. on Automated Software Engineering (ASE)","author":"K. Sen","year":"2007","unstructured":"Sen, K.: Effective random testing of concurrent programs. In: Stirewalt, R.E.K., Egyed, A., Fischer, B. (eds.) Intl. Conf. on Automated Software Engineering (ASE), pp.\u00a0323\u2013332. ACM, New York (2007)"},{"key":"19_CR133","first-page":"11","volume-title":"Conf. on Programming Language Design and Implementation (PLDI)","author":"K. Sen","year":"2008","unstructured":"Sen, K.: Race directed random testing of concurrent programs. In: Gupta, R., Amarasinghe, S.P. (eds.) Conf. on Programming Language Design and Implementation (PLDI), pp.\u00a011\u201321. ACM, New York (2008)"},{"key":"19_CR134","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"339","DOI":"10.1007\/11693017_25","volume-title":"Intl. Conf. on Fundamental Approaches to Software Engineering (FASE)","author":"K. Sen","year":"2006","unstructured":"Sen, K., Agha, G.: Automated systematic testing of open distributed programs. In: Baresi, L., Heckel, R. (eds.) Intl. Conf. on Fundamental Approaches to Software Engineering (FASE). LNCS, vol.\u00a03922, pp.\u00a0339\u2013356. Springer, Heidelberg (2006)"},{"key":"19_CR135","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"419","DOI":"10.1007\/11817963_38","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","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.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a04144, pp.\u00a0419\u2013423. Springer, Heidelberg (2006)"},{"key":"19_CR136","series-title":"LNCS","first-page":"166","volume-title":"Intl. Haifa Verification Conf. (HVC)","author":"K. Sen","year":"2006","unstructured":"Sen, K., Agha, G.: A race-detection and flipping algorithm for automated testing of multi-threaded programs. In: Bin, E., Ziv, A., Ur, S. (eds.) Intl. Haifa Verification Conf. (HVC). LNCS, vol.\u00a04383, pp.\u00a0166\u2013182. Springer, Heidelberg (2006)"},{"key":"19_CR137","first-page":"488","volume-title":"Intl. Symp. on Foundations of Software Engineering (FSE)","author":"K. Sen","year":"2013","unstructured":"Sen, K., Kalasapur, S., Brutch, T.G., Gibbs, S.: Jalangi: a selective record-replay and dynamic analysis framework for JavaScript. In: Meyer, B., Baresi, L., Mezini, M. (eds.) Intl. Symp. on Foundations of Software Engineering (FSE), pp.\u00a0488\u2013498. ACM, New York (2013)"},{"key":"19_CR138","first-page":"263","volume-title":"Intl. Symp. on Foundations of Software Engineering (FSE)","author":"K. Sen","year":"2005","unstructured":"Sen, K., Marinov, D., Agha, G.: CUTE: a concolic unit testing engine for C. In: Wermelinger, M., Gall, H.C. (eds.) Intl. Symp. on Foundations of Software Engineering (FSE), pp.\u00a0263\u2013272. ACM, New York (2005)"},{"key":"19_CR139","first-page":"157","volume-title":"Intl. Symp. on Software Testing and Analysis (ISSTA)","author":"S.F. Siegel","year":"2006","unstructured":"Siegel, S.F., Mironova, A., Avrunin, G.S., Clarke, L.A.: Using model checking with symbolic execution to verify parallel numerical programs. In: Pollock, L.L., Pezz\u00e8, M. (eds.) Intl. Symp. on Software Testing and Analysis (ISSTA), pp.\u00a0157\u2013168. ACM, New York (2006)"},{"key":"19_CR140","series-title":"LNCS","first-page":"1","volume-title":"International Conference on Information Systems Security (ICISS)","author":"D.X. Song","year":"2008","unstructured":"Song, D.X., Brumley, D., Yin, H., Caballero, J., Jager, I., Kang, M.G., Liang, Z., Newsome, J., Poosankam, P., Saxena, P.: BitBlaze: a new approach to computer security via binary analysis. In: Sekar, R., Pujari, A.K. (eds.) International Conference on Information Systems Security (ICISS). LNCS, vol.\u00a05352, pp.\u00a01\u201325. Springer, Heidelberg (2008)"},{"key":"19_CR141","series-title":"LNCS","volume-title":"Intl. Symp. on Model Checking of Software (SPIN)","author":"S.D. Stoller","year":"2000","unstructured":"Stoller, S.D.: Model-checking multi-threaded distributed java programs. In: Havelund, K., Penix, J., Visser, W. (eds.) Intl. Symp. on Model Checking of Software (SPIN). LNCS, vol.\u00a01885. Springer, Heidelberg (2000)"},{"issue":"5","key":"19_CR142","doi-asserted-by":"crossref","first-page":"362","DOI":"10.1145\/69586.69587","volume":"26","author":"R.N. Taylor","year":"1983","unstructured":"Taylor, R.N.: A general-purpose algorithm for analyzing concurrent programs. Commun. ACM 26(5), 362\u2013376 (1983)","journal-title":"Commun. ACM"},{"key":"19_CR143","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1007\/978-3-540-79124-9_10","volume-title":"Intl. Conf. on Tests and Proofs (TAP)","author":"N. Tillmann","year":"2008","unstructured":"Tillmann, N., de Halleux, J.: Pex\u2014white box test generation for net. In: Beckert, B., H\u00e4hnle, R. (eds.) Intl. Conf. on Tests and Proofs (TAP). LNCS, vol.\u00a04966, pp.\u00a0134\u2013153. Springer, Heidelberg (2008)"},{"key":"19_CR144","series-title":"LNCS","first-page":"491","volume-title":"International Conference on Applications and Theory of Petri Nets","author":"A. Valmari","year":"1989","unstructured":"Valmari, A.: Stubborn sets for reduced state space generation. In: Rozenberg, G. (ed.) International Conference on Applications and Theory of Petri Nets. LNCS, vol.\u00a0483, pp.\u00a0491\u2013515. Springer, Heidelberg (1989)"},{"key":"19_CR145","first-page":"332","volume-title":"Symp. on Logic in Computer Science (LICS)","author":"M.Y. Vardi","year":"1986","unstructured":"Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Symp. on Logic in Computer Science (LICS), pp.\u00a0332\u2013344. IEEE, Piscataway (1986)"},{"key":"19_CR146","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1007\/978-3-540-78917-8_2","volume-title":"Formal Methods and Testing","author":"M. Veanes","year":"2008","unstructured":"Veanes, M., Campbell, C., Grieskamp, W., Schulte, W., Tillmann, N., Nachmanson, L.: Model-based testing of object-oriented reactive systems with Spec Explorer. In: Hierons, R.M., Bowen, J.P., Harman, M. (eds.) Formal Methods and Testing. LNCS, vol.\u00a04949, pp.\u00a039\u201376. Springer, Heidelberg (2008)"},{"key":"19_CR147","series-title":"LNCS","first-page":"51","volume-title":"Analysis and Verification of Multiple-Agent Languages (LOMAPS)","author":"A. Venet","year":"1996","unstructured":"Venet, A.: Abstract interpretation of the pi-calculus. In: Dam, M. (ed.) Analysis and Verification of Multiple-Agent Languages (LOMAPS). LNCS, vol.\u00a01192, pp.\u00a051\u201375. Springer, Heidelberg (1996)"},{"key":"19_CR148","first-page":"3","volume-title":"Intl. Conf. on Automated Software Engineering (ASE)","author":"W. Visser","year":"2000","unstructured":"Visser, W., Havelund, K., Brat, G.P., Park, S.: Model checking programs. In: Intl. Conf. on Automated Software Engineering (ASE), pp.\u00a03\u201312. IEEE, Piscataway (2000)"},{"key":"19_CR149","first-page":"97","volume-title":"Intl. Symp. on Software Testing and Analysis (ISSTA)","author":"W. Visser","year":"2004","unstructured":"Visser, W., P\u0103s\u0103reanu, C.S., Khurshid, S.: Test input generation with Java PathFinder. In: Avrunin, G.S., Rothermel, G. (eds.) Intl. Symp. on Software Testing and Analysis (ISSTA), pp.\u00a097\u2013107. ACM, New York (2004)"},{"key":"19_CR150","first-page":"261","volume-title":"Symposium on Principles and Practice of Parallel Programming (PPOPP)","author":"A. Vo","year":"2009","unstructured":"Vo, A., Vakkalanka, S.S., Delisi, M., Gopalakrishnan, G., Kirby, R.M., Thakur, R.: Formal verification of practical MPI programs. In: Reed, D.A., Sarkar, V. (eds.) Symposium on Principles and Practice of Parallel Programming (PPOPP), pp.\u00a0261\u2013270. ACM, New York (2009)"},{"key":"19_CR151","first-page":"281","volume-title":"European Dependable Computing Conference (EDCC)","author":"N. Williams","year":"2005","unstructured":"Williams, N., Marre, B., Mouy, P., Roger, M.: Pathcrawler: automatic generation of path tests by combining static and dynamic analysis. In: Cin, M.D., Ka\u00e2niche, M., Pataricza, A. (eds.) European Dependable Computing Conference (EDCC), pp.\u00a0281\u2013292. Springer, Heidelberg (2005)"},{"key":"19_CR152","first-page":"27","volume-title":"Intl. Symp. on Software Testing and Analysis (ISSTA)","author":"R. Xu","year":"2008","unstructured":"Xu, R., Godefroid, P., Majumdar, R.: Testing for buffer overflows with length abstraction. In: Ryder, B.G., Zeller, A. (eds.) Intl. Symp. on Software Testing and Analysis (ISSTA), pp.\u00a027\u201338. ACM, New York (2008)"},{"key":"19_CR153","first-page":"213","volume-title":"USENIX Symp. on Networked Systems Design and Implementation (NSDI)","author":"J. Yang","year":"2009","unstructured":"Yang, J., Chen, T., Wu, M., Xu, Z., Liu, X., Lin, H., Yang, M., Long, F., Zhang, L., Zhou, L.: MODIST: transparent model checking of unmodified distributed systems. In: Rexford, J., Sirer, E.G. (eds.) USENIX Symp. on Networked Systems Design and Implementation (NSDI), pp.\u00a0213\u2013228. USENIX Association, Berkeley (2009)"},{"key":"19_CR154","first-page":"273","volume-title":"Operating Systems Design and Implementation (OSDI)","author":"J. Yang","year":"2004","unstructured":"Yang, J., Twohey, P., Engler, D.R., Musuvathi, M.: Using model checking to find serious file system errors. In: Brewer, E.A., Chen, P. (eds.) Operating Systems Design and Implementation (OSDI), pp.\u00a0273\u2013288. USENIX Association, Berkeley (2004)"},{"key":"19_CR155","first-page":"476","volume-title":"ACM Symp. on Theory of Computing (STOC)","author":"M. Yannakakis","year":"1991","unstructured":"Yannakakis, M., Lee, D.: Testing finite state machines (extended abstract). In: Koutsougeras, C., Vitter, J.S. (eds.) ACM Symp. on Theory of Computing (STOC), pp.\u00a0476\u2013485. ACM, New York (1991)"}],"container-title":["Handbook of Model Checking"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-10575-8_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,9,2]],"date-time":"2023-09-02T14:19:20Z","timestamp":1693664360000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-10575-8_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319105741","9783319105758"],"references-count":155,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-10575-8_19","relation":{},"subject":[],"published":{"date-parts":[[2018]]}}}