{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T21:05:36Z","timestamp":1776373536834,"version":"3.51.2"},"publisher-location":"Cham","reference-count":47,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319703886","type":"print"},{"value":"9783319703893","type":"electronic"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-70389-3_7","type":"book-chapter","created":{"date-parts":[[2017,11,11]],"date-time":"2017-11-11T14:42:30Z","timestamp":1510411350000},"page":"99-114","source":"Crossref","is-referenced-by-count":32,"title":["Software Verification: Testing vs. Model Checking"],"prefix":"10.1007","author":[{"given":"Dirk","family":"Beyer","sequence":"first","affiliation":[]},{"given":"Thomas","family":"Lemberger","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,11,12]]},"reference":[{"issue":"8","key":"7_CR1","doi-asserted-by":"crossref","first-page":"1978","DOI":"10.1016\/j.jss.2013.02.061","volume":"86","author":"S Anand","year":"2013","unstructured":"Anand, S., Burke, E.K., Chen, T.Y., Clark, J.A., Cohen, M.B., Grieskamp, W., Harman, M., Harrold, M.J., McMinn, P.: An orchestrated survey of methodologies for automated software test-case generation. Journal of Systems and Software 86(8), 1978\u20132001 (2013)","journal-title":"Journal of Systems and Software"},{"key":"7_CR2","doi-asserted-by":"crossref","unstructured":"Ball, T., Rajamani, S.K.: The Slam project: Debugging system software via static analysis. In: Proc. POPL, pp. 1\u20133. ACM (2002)","DOI":"10.1145\/503272.503274"},{"key":"7_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"504","DOI":"10.1007\/978-3-642-28756-5_38","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Beyer","year":"2012","unstructured":"Beyer, D.: Competition on software verification. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 504\u2013524. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28756-5_38"},{"key":"7_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1007\/978-3-662-54580-5_20","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Beyer","year":"2017","unstructured":"Beyer, D.: Software verification with validation of results. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10206, pp. 331\u2013349. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54580-5_20"},{"key":"7_CR5","doi-asserted-by":"crossref","unstructured":"Beyer, D., Chlipala, A.J., Henzinger, T.A., Jhala, R., Majumdar, R.: Generating tests from counterexamples. In: Proc. ICSE, pp. 326\u2013335. IEEE (2004)","DOI":"10.1109\/ICSE.2004.1317455"},{"key":"7_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"502","DOI":"10.1007\/978-3-319-41540-6_28","volume-title":"Computer Aided Verification","author":"D Beyer","year":"2016","unstructured":"Beyer, D., Dangl, M.: Verification-Aided debugging: An interactive web-service for exploring error witnesses. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9780, pp. 502\u2013509. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41540-6_28"},{"key":"7_CR7","doi-asserted-by":"crossref","unstructured":"Beyer, D., Dangl, M., Dietsch, D., Heizmann, M., Stahlbauer, A.: Witness validation and stepwise testification across software verifiers. In: Proc. FSE, pp. 721\u2013733. ACM (2015)","DOI":"10.1145\/2786805.2786867"},{"key":"7_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"622","DOI":"10.1007\/978-3-319-21690-4_42","volume-title":"Computer Aided Verification","author":"D Beyer","year":"2015","unstructured":"Beyer, D., Dangl, M., Wendler, P.: Boosting k-induction with continuously-refined invariants. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 622\u2013640. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_42"},{"issue":"5\u20136","key":"7_CR9","doi-asserted-by":"crossref","first-page":"505","DOI":"10.1007\/s10009-007-0044-z","volume":"9","author":"D Beyer","year":"2007","unstructured":"Beyer, D., Henzinger, T.A., Jhala, R., Majumdar, R.: The software model checker Blast. Int. J. Softw. Tools Technol. Transfer 9(5\u20136), 505\u2013525 (2007)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"7_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"472","DOI":"10.1007\/978-3-642-37036-6_26","volume-title":"Programming Languages and Systems","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.) ESOP 2013. LNCS, vol. 7792, pp. 472\u2013491. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-37036-6_26"},{"key":"7_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1007\/978-3-642-22110-1_16","volume-title":"Computer Aided Verification","author":"D Beyer","year":"2011","unstructured":"Beyer, D., Keremoglu, M.E.: CPAchecker: A tool for configurable software verification. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 184\u2013190. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_16"},{"key":"7_CR12","unstructured":"Beyer, D., Keremoglu, M.E., Wendler, P.: Predicate abstraction with adjustable-block encoding. In: Proc. FMCAD, pp. 189\u2013197. FMCAD (2010)"},{"key":"7_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/978-3-642-37057-1_11","volume-title":"Fundamental Approaches to Software Engineering","author":"D Beyer","year":"2013","unstructured":"Beyer, D., L\u00f6we, S.: Explicit-State software model checking based on cegar and interpolation. In: Cortellessa, V., Varr\u00f3, D. (eds.) FASE 2013. LNCS, vol. 7793, pp. 146\u2013162. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-37057-1_11"},{"key":"7_CR14","volume-title":"Reliable benchmarking: Requirements and solutions","author":"D Beyer","year":"2017","unstructured":"Beyer, D., L\u00f6we, S., Wendler, P.: Reliable benchmarking: Requirements and solutions. Int. J. Softw. Tools Technol, Transfer (2017)"},{"key":"7_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-39176-7_1","volume-title":"Model Checking Software","author":"D Beyer","year":"2013","unstructured":"Beyer, D., Wendler, P.: Reuse of verification results. In: Bartocci, E., Ramakrishnan, C.R. (eds.) SPIN 2013. LNCS, vol. 7976, pp. 1\u201317. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39176-7_1"},{"key":"7_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193\u2013207. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-49059-0_14"},{"key":"7_CR17","doi-asserted-by":"crossref","unstructured":"B\u00f6hme, M., Pham, V., Roychoudhury, A.: Coverage-based greybox fuzzing as Markov chain. In: Proc. SIGSAC, pp. 1032\u20131043. ACM (2016)","DOI":"10.1145\/2976749.2978428"},{"key":"7_CR18","doi-asserted-by":"crossref","unstructured":"Burnim, J., Sen, K.: Heuristics for scalable dynamic test generation. In: Proc. ASE, pp. 443\u2013446. IEEE (2008)","DOI":"10.1109\/ASE.2008.69"},{"key":"7_CR19","unstructured":"Cadar, C., Dunbar, D., Engler, D.R.: KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs. In: Proc. OSDI, pp. 209\u2013224. USENIX Association (2008)"},{"key":"7_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-642-36742-7_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Cimatti","year":"2013","unstructured":"Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The MathSAT5 SMT Solver. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 93\u2013107. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-36742-7_7"},{"issue":"5","key":"7_CR21","doi-asserted-by":"crossref","first-page":"752","DOI":"10.1145\/876638.876643","volume":"50","author":"EM Clarke","year":"2003","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. J. ACM 50(5), 752\u2013794 (2003)","journal-title":"J. ACM"},{"key":"7_CR22","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. 2988, pp. 168\u2013176. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24730-2_15"},{"key":"7_CR23","doi-asserted-by":"crossref","unstructured":"Craig, W.: Linear reasoning. A new form of the Herbrand-Gentzen theorem. J. Symb. Log. 22(3), 250\u2013268 )(1957)","DOI":"10.2307\/2963593"},{"key":"7_CR24","doi-asserted-by":"crossref","unstructured":"Csallner, C., Smaragdakis, Y.: Check \u2018n\u2019 crash: Combining static checking and testing. In: Proc. ICSE, pp. 422\u2013431. ACM (2005)","DOI":"10.1145\/1062455.1062533"},{"key":"7_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1007\/978-3-662-46681-0_34","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M Dangl","year":"2015","unstructured":"Dangl, M., L\u00f6we, S., Wendler, P.: CPAchecker with support for recursive programs and floating-point arithmetic. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 423\u2013425. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_34"},{"key":"7_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"502","DOI":"10.1007\/978-3-540-24605-3_37","volume-title":"Theory and Applications of Satisfiability Testing","author":"N E\u00e9n","year":"2004","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502\u2013518. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24605-3_37"},{"issue":"1","key":"7_CR27","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1007\/s10009-015-0407-9","volume":"19","author":"MYR Gadelha","year":"2017","unstructured":"Gadelha, M.Y.R., Ismail, H.I., Cordeiro, L.C.: Handling loops in bounded model checking of C programs via k-induction. STTT 19(1), 97\u2013114 (2017)","journal-title":"STTT"},{"issue":"6","key":"7_CR28","doi-asserted-by":"crossref","first-page":"727","DOI":"10.1007\/s10009-013-0272-3","volume":"16","author":"SJ Galler","year":"2014","unstructured":"Galler, S.J., Aichernig, B.K.: Survey on test data generation tools. STTT 16(6), 727\u2013751 (2014)","journal-title":"STTT"},{"key":"7_CR29","doi-asserted-by":"crossref","unstructured":"Godefroid, P., Klarlund, N., Sen, K.: Dart: Directed automated random testing. In: Proc. PLDI, pp. 213\u2013223. ACM (2005)","DOI":"10.1145\/1065010.1065036"},{"key":"7_CR30","unstructured":"Godefroid, P., Levin, M.Y., Molnar, D.A.: Automated whitebox fuzz testing. In: Proc. NDSS. The Internet Society (2008)"},{"key":"7_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","volume-title":"Computer Aided Verification","author":"S Graf","year":"1997","unstructured":"Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72\u201383. Springer, Heidelberg (1997). https:\/\/doi.org\/10.1007\/3-540-63166-6_10"},{"key":"7_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"455","DOI":"10.1007\/978-3-662-46681-0_43","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M Heizmann","year":"2015","unstructured":"Heizmann, M., Dietsch, D., Leike, J., Musa, B., Podelski, A.: Ultimate Automizer with array interpolation. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 455\u2013457. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_43"},{"key":"7_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1007\/978-3-642-39799-8_2","volume-title":"Computer Aided Verification","author":"M Heizmann","year":"2013","unstructured":"Heizmann, M., Hoenicke, J., Podelski, A.: Software model checking for people who love automata. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 36\u201352. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_2"},{"key":"7_CR34","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: Proc. POPL, pp. 58\u201370. ACM (2002)","DOI":"10.1145\/503272.503279"},{"key":"7_CR35","doi-asserted-by":"crossref","unstructured":"Holzer, A., Schallhart, C., Tautschnig, M., Veith, H.: How did you specify your test suite? In: Proc. ASE, pp. 407\u2013416. ACM (2010)","DOI":"10.1145\/1858996.1859084"},{"key":"7_CR36","unstructured":"Jayaraman, K., Harvison, D., Ganesh, V., Kiezun, A.: jFuzz: a concolic whitebox fuzzer for Java. In: Proc. NFM, pp. 121\u2013125 (2009)"},{"key":"7_CR37","doi-asserted-by":"crossref","unstructured":"Jhala, R., Majumdar, R.: Software model checking. ACM Computing Surveys 41(4) (2009)","DOI":"10.1145\/1592434.1592438"},{"key":"7_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1007\/978-3-642-11486-1_14","volume-title":"Perspectives of Systems Informatics","author":"A Khoroshilov","year":"2010","unstructured":"Khoroshilov, A., Mutilin, V., Petrenko, A., Zakharov, V.: Establishing Linux driver verification process. In: Pnueli, A., Virbitskaite, I., Voronkov, A. (eds.) PSI 2009. LNCS, vol. 5947, pp. 165\u2013176. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-11486-1_14"},{"key":"7_CR39","unstructured":"K\u00f6roglu, Y., Sen, A.: Design of a modified concolic testing algorithm with smaller constraints. In: Proc. ISSTA, pp. 3\u201314. ACM (2016)"},{"key":"7_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"389","DOI":"10.1007\/978-3-642-54862-8_26","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Kroening","year":"2014","unstructured":"Kroening, D., Tautschnig, M.: CBMC \u2013 C bounded model checker (competition contribution). In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 389\u2013391. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54862-8_26"},{"key":"7_CR41","doi-asserted-by":"crossref","unstructured":"Li, K., Reichenbach, C., Csallner, C., Smaragdakis, Y.: Residual investigation: Predictive and precise bug detection. In: Proc. ISSTA, pp. 298\u2013308. ACM (2012)","DOI":"10.1145\/2338965.2336789"},{"key":"7_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-45069-6_1","volume-title":"Computer Aided Verification","author":"KL McMillan","year":"2003","unstructured":"McMillan, K.L.: Interpolation and SAT-based model checking. In: Hunt, W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 1\u201313. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-45069-6_1"},{"key":"7_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"405","DOI":"10.1007\/978-3-642-54862-8_31","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J Morse","year":"2014","unstructured":"Morse, J., Ramalho, M., Cordeiro, L., Nicole, D., Fischer, B.: ESBMC 1.22 (competition contribution). In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 405\u2013407. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54862-8_31"},{"key":"7_CR44","doi-asserted-by":"crossref","unstructured":"Pavlinovic, Z., Lal, A., Sharma, R.: Inferring annotations for device drivers from verification histories. In: Proc. ASE, pp. 450\u2013460. ACM (2016)","DOI":"10.1145\/2970276.2970305"},{"key":"7_CR45","doi-asserted-by":"crossref","unstructured":"Sen, K., Marinov, D., Agha, G.: Cute: A concolic unit testing engine for C. In: Proc. ESEC\/FSE, pp. 263\u2013272. ACM (2005)","DOI":"10.1145\/1081706.1081750"},{"key":"7_CR46","doi-asserted-by":"crossref","unstructured":"Seo, H., Kim, S.: How we get there: A context-guided search strategy in concolic testing. In: Proc. FSE, pp. 413\u2013424. ACM (2014)","DOI":"10.1145\/2635868.2635872"},{"issue":"1","key":"7_CR47","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1134\/S0361768815010065","volume":"41","author":"IS Zakharov","year":"2015","unstructured":"Zakharov, I.S., Mandrykin, M.U., Mutilin, V.S., Novikov, E., Petrenko, A.K., Khoroshilov, A.V.: Configurable toolset for static verification of operating systems kernel modules. Programming and Computer Software 41(1), 49\u201364 (2015)","journal-title":"Programming and Computer Software"}],"container-title":["Lecture Notes in Computer Science","Hardware and Software: Verification and Testing"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-70389-3_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,6]],"date-time":"2019-10-06T01:29:25Z","timestamp":1570325365000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-70389-3_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319703886","9783319703893"],"references-count":47,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-70389-3_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]}}}