{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T15:19:03Z","timestamp":1743002343758,"version":"3.40.3"},"publisher-location":"Cham","reference-count":20,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319229683"},{"type":"electronic","value":"9783319229690"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-22969-0_9","type":"book-chapter","created":{"date-parts":[[2015,8,20]],"date-time":"2015-08-20T08:51:42Z","timestamp":1440060702000},"page":"117-131","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Efficient Testing of Different Loop Paths"],"prefix":"10.1007","author":[{"given":"Stefan","family":"Huster","sequence":"first","affiliation":[]},{"given":"Sebastian","family":"Burg","sequence":"additional","affiliation":[]},{"given":"Hanno","family":"Eichelberger","sequence":"additional","affiliation":[]},{"given":"Jo","family":"Laufenberg","sequence":"additional","affiliation":[]},{"given":"J\u00fcrgen","family":"Ruf","sequence":"additional","affiliation":[]},{"given":"Thomas","family":"Kropf","sequence":"additional","affiliation":[]},{"given":"Wolfgang","family":"Rosenstiel","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,8,21]]},"reference":[{"key":"9_CR1","doi-asserted-by":"crossref","unstructured":"Xiao, X., Li, S., Xie, T., Tillmann, N.: Characteristic studies of loop problems for structural test generation via symbolic execution. In: Proceedings of 28th IEEE\/ACM International Conference on Automated Software Engineering (ASE 2013), November 2013","DOI":"10.1109\/ASE.2013.6693084"},{"key":"9_CR2","doi-asserted-by":"crossref","unstructured":"Liu, T., Nagel, M., Taghdiri, M.: Bounded program verification using an SMT solver: a case study. In: 2012 IEEE Fifth International Conference on Software Testing, Verification and Validation (ICST), pp. 101\u2013110. IEEE (2012)","DOI":"10.1109\/ICST.2012.90"},{"key":"9_CR3","unstructured":"Godefroid, P., Levin, M.Y., Molnar, D.A., et al.: Automated whitebox fuzz testing. In: NDSS, vol. 8, pp. 151\u2013166 (2008)"},{"issue":"7","key":"9_CR4","doi-asserted-by":"publisher","first-page":"1165","DOI":"10.1109\/TCAD.2008.923410","volume":"27","author":"V D\u2019silva","year":"2008","unstructured":"D\u2019silva, V., Kroening, D., Weissenbacher, G.: A survey of automated techniques for formal software verification. IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst. 27(7), 1165\u20131178 (2008)","journal-title":"IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst."},{"key":"9_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/978-3-540-30569-9_6","volume-title":"Construction and Analysis of Safe, Secure, and Interoperable Smart Devices","author":"DR Cok","year":"2005","unstructured":"Cok, D.R., Kiniry, J.R.: ESC\/Java2: uniting ESC\/Java and JML. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol. 3362, pp. 108\u2013128. Springer, Heidelberg (2005)"},{"key":"9_CR6","doi-asserted-by":"crossref","unstructured":"Blanc, R., Kuncak, V., Kneuss, E., Suter, P.: An overview of the Leon verification system: verification by translation to recursive functions. In: Proceedings of the 4th Workshop on Scala, p. 1. ACM (2013)","DOI":"10.1145\/2489837.2489838"},{"key":"9_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"340","DOI":"10.1007\/978-3-319-10428-7_26","volume-title":"Principles and Practice of Constraint Programming","author":"K Francis","year":"2014","unstructured":"Francis, K., Stuckey, P.J.: Loop untangling. In: O\u2019Sullivan, B. (ed.) CP 2014. LNCS, vol. 8656, pp. 340\u2013355. Springer, Heidelberg (2014)"},{"key":"9_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"281","DOI":"10.1007\/11408901_21","volume-title":"Dependable Computing - EDCC 2005","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: Dal Cin, M., Ka\u00e2niche, M., Pataricza, A. (eds.) EDCC 2005. LNCS, vol. 3463, pp. 281\u2013292. Springer, Heidelberg (2005)"},{"issue":"6","key":"9_CR9","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1145\/1064978.1065036","volume":"40","author":"P Godefroid","year":"2005","unstructured":"Godefroid, P., Klarlund, N., Sen, K.: Dart: directed automated random testing. SIGPLAN Not. 40(6), 213\u2013223 (2005). DirectedTesting","journal-title":"SIGPLAN Not."},{"key":"9_CR10","doi-asserted-by":"crossref","unstructured":"Xie, T., Tillmann, N., de Halleux, J., Schulte, W.: Fitness-guided path exploration in dynamic symbolic execution. In: IEEE\/IFIP International Conference on Dependable Systems Networks, DSN 2009, pp. 359\u2013368, June 2009","DOI":"10.1109\/DSN.2009.5270315"},{"key":"9_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1007\/978-3-642-24372-1_34","volume-title":"Automated Technology for Verification and Analysis","author":"J Obdr\u017e\u00e1lek","year":"2011","unstructured":"Obdr\u017e\u00e1lek, J., Trt\u00edk, M.: Efficient loop navigation for symbolic execution. In: Bultan, T., Hsiung, P.-A. (eds.) ATVA 2011. LNCS, vol. 6996, pp. 453\u2013462. Springer, Heidelberg (2011)"},{"key":"9_CR12","doi-asserted-by":"crossref","unstructured":"Godefroid, P., Luchaup, D.: Automatic partial loop summarization in dynamic test generation. In: Proceedings of the 2011 International Symposium on Software Testing and Analysis, ISSTA 2011, pp. 23\u201333. ACM, New York (2011)","DOI":"10.1145\/2001420.2001424"},{"key":"9_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1007\/978-3-642-23702-7_26","volume-title":"Static Analysis","author":"AF Donaldson","year":"2011","unstructured":"Donaldson, A.F., Haller, L., Kroening, D., R\u00fcmmer, P.: Software verification using k-induction. In: Yahav, E. (ed.) Static Analysis. LNCS, vol. 6887, pp. 351\u2013368. Springer, Heidelberg (2011)"},{"key":"9_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/978-3-642-19835-9_9","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Tsitovich","year":"2011","unstructured":"Tsitovich, A., Sharygina, N., Wintersteiger, C.M., Kroening, D.: Loop summarization and termination analysis. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 81\u201395. Springer, Heidelberg (2011)"},{"issue":"1","key":"9_CR15","doi-asserted-by":"publisher","first-page":"78","DOI":"10.1504\/IJCCBS.2014.059596","volume":"5","author":"A Louhichi","year":"2014","unstructured":"Louhichi, A., Ghardallou, W., Bsaies, K., Jilani, L.L., Mraihi, O., Mili, A.: Verifying while loops with invariant relations. Int. J. Crit. Comput.-Based Syst. 5(1), 78\u2013102 (2014)","journal-title":"Int. J. Crit. Comput.-Based Syst."},{"key":"9_CR16","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 Kroning","year":"2004","unstructured":"Kroning, D., Groce, A., Clarke, E.: Counterexample guided abstraction refinement via program execution. In: Davies, J., Schulte, W., Barnett, M. (eds.) ICFEM 2004. LNCS, vol. 3308, pp. 224\u2013238. Springer, Heidelberg (2004)"},{"issue":"2","key":"9_CR17","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1007\/s00165-009-0110-2","volume":"22","author":"D Kroening","year":"2010","unstructured":"Kroening, D., Weissenbacher, G.: Verification and falsification of programs with loops using predicate abstraction. Formal Aspects Comput. 22(2), 105\u2013128 (2010)","journal-title":"Formal Aspects Comput."},{"issue":"5","key":"9_CR18","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1109\/MS.2008.109","volume":"25","author":"P Godefroid","year":"2008","unstructured":"Godefroid, P., de Halleux, P., Nori, A.V., Rajamani, S.K., Schulte, W., Tillmann, N., Levin, M.Y.: Automating software testing using program analysis. IEEE Softw. 25(5), 30\u201337 (2008)","journal-title":"IEEE Softw."},{"issue":"1","key":"9_CR19","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1002\/stvr.309","volume":"15","author":"G Lee","year":"2005","unstructured":"Lee, G., Morris, J., Parker, K., Bundell, G.A., Lam, P.: Using symbolic execution to guide test generation. Softw. Test. Verification Reliab. 15(1), 41\u201361 (2005)","journal-title":"Softw. Test. Verification Reliab."},{"key":"9_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.S.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008)"}],"container-title":["Lecture Notes in Computer Science","Software Engineering and Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-22969-0_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,20]],"date-time":"2023-01-20T19:54:23Z","timestamp":1674244463000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-22969-0_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319229683","9783319229690"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-22969-0_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"21 August 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}