{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,24]],"date-time":"2025-06-24T06:27:46Z","timestamp":1750746466821,"version":"3.41.0"},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662466742"},{"type":"electronic","value":"9783662466759"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-662-46675-9_7","type":"book-chapter","created":{"date-parts":[[2015,3,31]],"date-time":"2015-03-31T20:24:38Z","timestamp":1427833478000},"page":"100-114","source":"Crossref","is-referenced-by-count":27,"title":["Just Test What You Cannot Verify!"],"prefix":"10.1007","author":[{"given":"Mike","family":"Czech","sequence":"first","affiliation":[]},{"given":"Marie-Christine","family":"Jakobs","sequence":"additional","affiliation":[]},{"given":"Heike","family":"Wehrheim","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"7_CR1","unstructured":"Gnu compiler collection, https:\/\/gcc.gnu.org (accessed: October 13, 2014)"},{"issue":"11-13","key":"7_CR2","doi-asserted-by":"publisher","first-page":"1372","DOI":"10.1016\/j.tcs.2009.10.025","volume":"411","author":"R.W. Barraclough","year":"2010","unstructured":"Barraclough, R.W., Binkley, D., Danicic, S., Harman, M., Hierons, R.M., Kiss, \u00c1., Laurence, M., Ouarbya, L.: A trajectory-based strict semantics for program slicing. Theoretical Computer Science\u00a0411(11-13), 1372\u20131386 (2010)","journal-title":"Theoretical Computer Science"},{"key":"7_CR3","doi-asserted-by":"crossref","unstructured":"Beckman, N.E., Nori, A.V., Rajamani, S.K., Simmons, R.J.: Proofs from tests. In: ISSTA 2008, pp. 3\u201314. ACM (2008)","DOI":"10.1145\/1390630.1390634"},{"key":"7_CR4","doi-asserted-by":"crossref","unstructured":"Bertolino, A.: Software testing research: Achievements, challenges, dreams. In: Briand, L.C., Wolf, A.L. (eds.) International Conference on Software Engineering, ISCE 2007, Workshop on the Future of Software Engineering, FOSE 2007, Minneapolis, MN, USA, May 23-25, pp. 85\u2013103 (2007)","DOI":"10.1109\/FOSE.2007.25"},{"key":"7_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"373","DOI":"10.1007\/978-3-642-54862-8_25","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D. Beyer","year":"2014","unstructured":"Beyer, D.: Status report on software verification. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014 (ETAPS). LNCS, vol.\u00a08413, pp. 373\u2013388. Springer, Heidelberg (2014)"},{"key":"7_CR6","doi-asserted-by":"crossref","unstructured":"Beyer, D., Chlipala, A.J., Henzinger, T.A., Jhala, R., Majumdar, R.: Generating tests from counterexamples. In: ICSE 2004, pp. 326\u2013335. IEEE Computer Society (2004)","DOI":"10.1109\/ICSE.2004.1317455"},{"key":"7_CR7","doi-asserted-by":"crossref","unstructured":"Beyer, D., Henzinger, T.A., Keremoglu, M.E., Wendler, P.: Conditional model checking: A technique to pass information between verifiers. In: FSE 2012, pp. 1\u201311. ACM (2012)","DOI":"10.1145\/2393596.2393664"},{"key":"7_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"504","DOI":"10.1007\/978-3-540-73368-3_51","volume-title":"Computer Aided Verification","author":"D. Beyer","year":"2007","unstructured":"Beyer, D., Henzinger, T.A., Th\u00e9oduloz, G.: Configurable software verification: Concretizing the convergence of model checking and program analysis. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 504\u2013518. Springer, Heidelberg (2007)"},{"key":"7_CR9","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.\u00a06806, pp. 184\u2013190. Springer, Heidelberg (2011)"},{"key":"7_CR10","unstructured":"Cadar, C., Dunbar, D., Engler, D.: KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. In: OSDI 2008, pp. 209\u2013224. USENIX Association (2008)"},{"issue":"11-12","key":"7_CR11","doi-asserted-by":"publisher","first-page":"595","DOI":"10.1016\/S0950-5849(98)00086-X","volume":"40","author":"G. Canfora","year":"1998","unstructured":"Canfora, G., Cimitile, A., De Lucia, A.: Conditioned program slicing. Information and Software Technology\u00a040(11-12), 595\u2013607 (1998)","journal-title":"Information and Software Technology"},{"key":"7_CR12","doi-asserted-by":"crossref","unstructured":"Chebaro, O., Kosmatov, N., Giorgetti, A., Julliand, J.: Program slicing enhances a verification technique combining static and dynamic analysis. In: SAC 2012, pp. 1284\u20131291. ACM (2012)","DOI":"10.1145\/2245276.2231980"},{"key":"7_CR13","doi-asserted-by":"crossref","unstructured":"Chen, J., MacDonald, S.: Towards a better collaboration of static and dynamic analyses for testing concurrent programs. In: PADTAD 2008, pp. 8:1\u20138:9. ACM (2008)","DOI":"10.1145\/1390841.1390849"},{"key":"7_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"132","DOI":"10.1007\/978-3-642-32759-9_13","volume-title":"FM 2012: Formal Methods","author":"M. Christakis","year":"2012","unstructured":"Christakis, M., M\u00fcller, P., W\u00fcstholz, V.: Collaborative verification and testing with explicit assumptions. In: Giannakopoulou, D., M\u00e9ry, D. (eds.) FM 2012. LNCS, vol.\u00a07436, pp. 132\u2013146. Springer, Heidelberg (2012)"},{"key":"7_CR15","doi-asserted-by":"crossref","unstructured":"Csallner, C., Smaragdakis, Y.: Check \u2019N\u2019 Crash: Combining static checking and testing. In: ICSE 2005, pp. 422\u2013431. ACM (2005)","DOI":"10.1145\/1062455.1062533"},{"key":"7_CR16","doi-asserted-by":"crossref","unstructured":"Csallner, C., Smaragdakis, Y.: DSD-Crasher: A hybrid analysis tool for bug finding. In: ISSTA 2006, pp. 245\u2013254. ACM (2006)","DOI":"10.1145\/1146238.1146267"},{"key":"7_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/978-3-642-33826-7_16","volume-title":"Software Engineering and Formal Methods","author":"P. Cuoq","year":"2012","unstructured":"Cuoq, P., Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-c. In: Eleftherakis, G., Hinchey, M., Holcombe, M. (eds.) SEFM 2012. LNCS, vol.\u00a07504, pp. 233\u2013247. Springer, Heidelberg (2012)"},{"key":"7_CR18","doi-asserted-by":"crossref","unstructured":"Ge, X., Taneja, K., Xie, T., Tillmann, N.: DyTa: Dynamic symbolic execution guided with static verification results. In: ICSE 2011, pp. 992\u2013994. ACM (2011)","DOI":"10.1145\/1985793.1985971"},{"key":"7_CR19","doi-asserted-by":"crossref","unstructured":"Gulavani, B.S., Henzinger, T.A., Kannan, Y., Nori, A.V., Rajamani, S.K.: SYNERGY: a new algorithm for property checking. In: SIGSOFT FSE 2006, pp. 117\u2013127. ACM Press (2006)","DOI":"10.1145\/1181775.1181790"},{"issue":"2","key":"7_CR20","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1007\/s00165-005-0059-8","volume":"17","author":"E. Gunter","year":"2005","unstructured":"Gunter, E., Peled, D.: Model checking, testing and verification working together. Formal Aspects of Computing\u00a017(2), 201\u2013221 (2005)","journal-title":"Formal Aspects of Computing"},{"key":"7_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"262","DOI":"10.1007\/978-3-642-00768-2_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Gupta","year":"2009","unstructured":"Gupta, A., Majumdar, R., Rybalchenko, A.: From tests to proofs. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol.\u00a05505, pp. 262\u2013276. Springer, Heidelberg (2009)"},{"key":"7_CR22","doi-asserted-by":"crossref","unstructured":"Harman, M., Hierons, R., Fox, C., Danicic, S., Howroyd, J.: Pre\/post conditioned slicing. In: ICSM 2001, pp. 138\u2013147 (2001)","DOI":"10.1109\/ICSM.2001.972724"},{"key":"7_CR23","doi-asserted-by":"crossref","unstructured":"Horwitz, S., Reps, T., Binkley, D.: Interprocedural slicing using dependence graphs. In: PLDI 1988, pp. 35\u201346. ACM (1988)","DOI":"10.1145\/960116.53994"},{"key":"7_CR24","doi-asserted-by":"crossref","unstructured":"Jalote, P., Vangala, V., Singh, T., Jain, P.: Program partitioning: A framework for combining static and dynamic analysis. In: WODA 2006, pp. 11\u201316. ACM (2006)","DOI":"10.1145\/1138912.1138916"},{"key":"7_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"224","DOI":"10.1007\/978-3-540-30482-1_23","volume-title":"Formal Methods and Software Engineering","author":"D. Kroening","year":"2004","unstructured":"Kroening, D., Groce, A., Clarke, E.: Counterexample guided abstraction refinement via program execution. In: Davies, J., Schulte, W., Barnett, M. (eds.) ICFEM 2004. LNCS, vol.\u00a03308, pp. 224\u2013238. Springer, Heidelberg (2004)"},{"key":"7_CR26","doi-asserted-by":"crossref","unstructured":"Ku, K., Hart, T.E., Chechik, M., Lie, D.: A buffer overflow benchmark for software model checkers. In: ASE 2007, pp. 389\u2013392. ACM (2007)","DOI":"10.1145\/1321631.1321691"},{"key":"7_CR27","doi-asserted-by":"crossref","unstructured":"Naik, M., Yang, H., Castelnuovo, G., Sagiv, M.: Abstractions from tests. In: POPL 2012, pp. 373\u2013386. ACM (2012)","DOI":"10.1145\/2103621.2103701"},{"key":"7_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/3-540-45937-5_16","volume-title":"Compiler Construction","author":"G.C. Necula","year":"2002","unstructured":"Necula, G.C., McPeak, S., Rahul, S.P., Weimer, W.: CIL: Intermediate language and tools for analysis and transformation of C programs. In: Nigel Horspool, R. (ed.) CC 2002. LNCS, vol.\u00a02304, pp. 213\u2013228. Springer, Heidelberg (2002)"},{"key":"7_CR29","doi-asserted-by":"crossref","unstructured":"Pastore, F., Mariani, L., Hyv\u00e4rinen, A.E.J., Fedyukovich, G., Sharygina, N., Sehestedt, S., Muhammad, A.: Verification-aided regression testing. In: ISSTA 2014, pp. 37\u201348. ACM (2014)","DOI":"10.1145\/2610384.2610387"},{"key":"7_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/978-3-540-24704-3_11","volume-title":"Testing of Communicating Systems","author":"V. Rusu","year":"2004","unstructured":"Rusu, V., Marchand, H., Tschaen, V., J\u00e9ron, T., Jeannet, B.: From safety verification to safety testing. In: Groz, R., Hierons, R.M. (eds.) TestCom 2004. LNCS, vol.\u00a02978, pp. 160\u2013176. Springer, Heidelberg (2004)"},{"key":"7_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"611","DOI":"10.1007\/3-540-45251-6_35","volume-title":"FME 2001: Formal Methods for Increasing Software Productivity","author":"N. Sharygina","year":"2001","unstructured":"Sharygina, N., Peled, D.: A combined testing and verification approach for software reliability. In: Oliveira, J.N., Zave, P. (eds.) FME 2001. LNCS, vol.\u00a02021, pp. 611\u2013628. Springer, Heidelberg (2001)"},{"key":"7_CR32","unstructured":"Tip, F.: A survey of program slicing techniques. Journal of Programming Languages\u00a03(3) (1995)"},{"key":"7_CR33","doi-asserted-by":"crossref","unstructured":"Yorsh, G., Ball, T., Sagiv, M.: Testing, abstraction, theorem proving: Better together? In: ISSTA 2006, pp. 145\u2013156. ACM (2006)","DOI":"10.1145\/1146238.1146255"}],"container-title":["Lecture Notes in Computer Science","Fundamental Approaches to Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-46675-9_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,21]],"date-time":"2025-05-21T19:47:53Z","timestamp":1747856873000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-46675-9_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783662466742","9783662466759"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-46675-9_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}