{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T22:29:23Z","timestamp":1743114563696,"version":"3.40.3"},"publisher-location":"Cham","reference-count":25,"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_18","type":"book-chapter","created":{"date-parts":[[2015,8,20]],"date-time":"2015-08-20T08:51:42Z","timestamp":1440060702000},"page":"251-267","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Memory Management Test-Case Generation of C Programs Using Bounded Model Checking"],"prefix":"10.1007","author":[{"given":"Herbert","family":"Rocha","sequence":"first","affiliation":[]},{"given":"Raimundo","family":"Barreto","sequence":"additional","affiliation":[]},{"given":"Lucas","family":"Cordeiro","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,8,21]]},"reference":[{"key":"18_CR1","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"18_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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. 8413, pp. 373\u2013388. Springer, Heidelberg (2014)"},{"key":"18_CR3","unstructured":"Beyer, D.: Competition on Software Verification (SV-COMP) - Results of the Competition (2015). http:\/\/sv-comp.sosy-lab.org\/2015\/results\/MemorySafety.table.html"},{"key":"18_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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)"},{"key":"18_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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., Kroning, 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)"},{"key":"18_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/978-3-540-88009-7","volume-title":"25 Years of Model Checking","author":"EM Clarke","year":"2008","unstructured":"Clarke, E.M.: The birth of model checking. In: Grumberg, Orna, Veith, Helmut (eds.) 25 Years of Model Checking. LNCS, vol. 5000, pp. 1\u201326. Springer, Heidelberg (2008)"},{"key":"18_CR7","doi-asserted-by":"crossref","unstructured":"Clause, J., Orso, A.: LEAKPOINT: pinpointing the causes of memory leaks. In: ICSE, pp. 515\u2013524. ACM (2010)","DOI":"10.1145\/1806799.1806874"},{"key":"18_CR8","unstructured":"Comar, C., Kanig, J., Moy, Y.: Integrating formal program verification with testing. In: ERTS (2012)"},{"key":"18_CR9","doi-asserted-by":"crossref","unstructured":"Cordeiro, L., Fischer, B., Marques-Silva, J.: SMT-Based bounded model checking for embedded ANSI-C software. In: TSE, pp. 957\u2013974. IEEE (2012)","DOI":"10.1109\/TSE.2011.59"},{"key":"18_CR10","doi-asserted-by":"crossref","unstructured":"Delahaye, M., Kosmatov, N., Signoles, J.: Common specification language for static and dynamic analysis of C programs. In: SAC, pp. 1230\u20131235. ACM (2013)","DOI":"10.1145\/2480362.2480593"},{"key":"18_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"412","DOI":"10.1007\/978-3-642-54862-8_33","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K Dudka","year":"2014","unstructured":"Dudka, K., Peringer, P., Vojnar, T.: Predator: a shape analyzer based on symbolic memory graphs. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014 (ETAPS). LNCS, vol. 8413, pp. 412\u2013414. Springer, Heidelberg (2014)"},{"key":"18_CR12","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Saxe, J.B.: Avoiding exponential explosion: generating compact verification conditions. In: POPL, pp. 193\u2013205. ACM (2001)","DOI":"10.1145\/373243.360220"},{"key":"18_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"142","DOI":"10.1007\/978-3-540-78163-9_15","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A Groce","year":"2008","unstructured":"Groce, A., Joshi, R.: Extending model checking with dynamic analysis. In: Logozzo, F., Peled, D.A., Zuck, L.D. (eds.) VMCAI 2008. LNCS, vol. 4905, pp. 142\u2013156. Springer, Heidelberg (2008)"},{"key":"18_CR14","unstructured":"Holik, L., Hruska, M., Lengal, O., Rogalewicz, A., Simacek, J., Vojnar, T.: Forester, (2015). http:\/\/www.fit.vutbr.cz\/research\/groups\/verifit\/tools\/forester\/"},{"key":"18_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"209","DOI":"10.1007\/978-3-540-70545-1_20","volume-title":"Computer Aided Verification","author":"A Holzer","year":"2008","unstructured":"Holzer, A., Schallhart, C., Tautschnig, M., Veith, H.: FShell: systematic test case generation for dynamic analysis and measurement. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 209\u2013213. Springer, Heidelberg (2008)"},{"key":"18_CR16","unstructured":"Kahsai, T., Gurfinkel, A., Navas, J.A.: SeaHorn - A software verification tool (2015). https:\/\/bitbucket.org\/lememta\/seahorn\/wiki\/Home"},{"key":"18_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1007\/978-3-642-04761-9_9","volume-title":"Automated Technology for Verification and Analysis","author":"M Kebrt","year":"2009","unstructured":"Kebrt, M., \u0160er\u00fd, O.: UnitCheck: unit testing and model checking combined. In: Liu, Z., Ravn, A.P. (eds.) ATVA 2009. LNCS, vol. 5799, pp. 97\u2013103. Springer, Heidelberg (2009)"},{"key":"18_CR18","unstructured":"Kumar, A.: CUnit (2014). http:\/\/cunit.sourceforge.net\/"},{"key":"18_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"146","DOI":"10.1007\/978-3-642-27705-4_12","volume-title":"Verified Software: Theories, Tools, Experiments","author":"F Merz","year":"2012","unstructured":"Merz, F., Falke, S., Sinz, C.: LLBMC: bounded model checking of C and C++ programs using a compiler IR. In: Joshi, R., M\u00fcller, P., Podelski, A. (eds.) VSTTE 2012. LNCS, vol. 7152, pp. 146\u2013161. Springer, Heidelberg (2012)"},{"key":"18_CR20","volume-title":"The Art of Software Testing","author":"GJ Myers","year":"2004","unstructured":"Myers, G.J., Sandler, C.: The Art of Software Testing. Wiley, New York (2004)"},{"key":"18_CR21","doi-asserted-by":"crossref","unstructured":"Nagarakatte, S., Zhao, J., Martin, M.M., Zdancewic, S.: CETS: compiler enforced temporal safety for C. In: ISMM, pp. 31\u201340. ACM (2010)","DOI":"10.1145\/1837855.1806657"},{"key":"18_CR22","doi-asserted-by":"crossref","unstructured":"Nethercote, N., Seward, J.: Valgrind: a framework for heavyweight dynamic binary instrumentation. In: PLDI, pp. 89\u2013100. ACM (2007)","DOI":"10.1145\/1273442.1250746"},{"key":"18_CR23","unstructured":"Rocha, H., Cordeiro, L., Barreto, R., Netto, J.: Exploiting safety properties in bounded model checking for test cases generation of C programs. In: SAST, pp. 121\u2013130. SBC (2010)"},{"key":"18_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"208","DOI":"10.1007\/978-3-319-08587-6_15","volume-title":"Automated Reasoning","author":"T Str\u00f6der","year":"2014","unstructured":"Str\u00f6der, T., Giesl, J., Brockschmidt, M., Frohn, F., Fuhs, C., Hensel, J., Schneider-Kamp, P.: Proving termination and memory safety for programs with pointer arithmetic. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS, vol. 8562, pp. 208\u2013223. Springer, Heidelberg (2014)"},{"key":"18_CR25","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)"}],"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_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,8]],"date-time":"2023-02-08T16:26:42Z","timestamp":1675873602000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-22969-0_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319229683","9783319229690"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-22969-0_18","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"}}]}}