{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T11:59:50Z","timestamp":1725796790678},"publisher-location":"Cham","reference-count":19,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319090986"},{"type":"electronic","value":"9783319090993"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-09099-3_16","type":"book-chapter","created":{"date-parts":[[2014,7,7]],"date-time":"2014-07-07T07:41:03Z","timestamp":1404718863000},"page":"204-211","source":"Crossref","is-referenced-by-count":9,"title":["How Test Generation Helps Software Specification and Deductive Verification in Frama-C"],"prefix":"10.1007","author":[{"given":"Guillaume","family":"Petiot","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nikolai","family":"Kosmatov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alain","family":"Giorgetti","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jacques","family":"Julliand","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"16_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/978-3-642-13977-2_4","volume-title":"Tests and Proofs","author":"K.Y. Ahn","year":"2010","unstructured":"Ahn, K.Y., Denney, E.: Testing first-order logic axioms in program verification. In: Fraser, G., Gargantini, A. (eds.) TAP 2010. LNCS, vol.\u00a06143, pp. 22\u201337. Springer, Heidelberg (2010)"},{"unstructured":"Baudin, P., Cuoq, P., Filli\u00e2tre, J.C., March\u00e9, C., Monate, B., Moy, Y., Prevosto, V.: ACSL: ANSI\/ISO C Specification Language, \n                  \n                    http:\/\/frama-c.com\/acsl.html","key":"16_CR2"},{"doi-asserted-by":"crossref","unstructured":"Beyer, D., Henzinger, T., Theoduloz, G.: Program analysis with dynamic precision adjustment. In: ASE (2008)","key":"16_CR3","DOI":"10.1109\/ASE.2008.13"},{"doi-asserted-by":"crossref","unstructured":"Botella, B., Delahaye, M., Hong Tuan Ha, S., Kosmatov, N., Mouy, P., Roger, M., Williams, N.: Automating structural testing of C programs: Experience with PathCrawler. In: AST (2009)","key":"16_CR4","DOI":"10.1109\/IWAST.2009.5069043"},{"doi-asserted-by":"crossref","unstructured":"Brucker, A.D., Wolff, B.: On theorem prover-based testing. FAC (2012)","key":"16_CR5","DOI":"10.1007\/s00165-012-0222-y"},{"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)","key":"16_CR6","DOI":"10.1145\/2245276.2231980"},{"key":"16_CR7","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":"16_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1007\/978-3-540-79124-9_5","volume-title":"Tests and Proofs","author":"K. Claessen","year":"2008","unstructured":"Claessen, K., Svensson, H.: Finding counter examples in induction proofs. In: Beckert, B., H\u00e4hnle, R. (eds.) TAP 2008. LNCS, vol.\u00a04966, pp. 48\u201365. Springer, Heidelberg (2008)"},{"key":"16_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/978-3-642-32469-7_8","volume-title":"Formal Methods for Industrial Critical Systems","author":"L. Correnson","year":"2012","unstructured":"Correnson, L., Signoles, J.: Combining analyses for C program verification. In: Stoelinga, M., Pinger, R. (eds.) FMICS 2012. LNCS, vol.\u00a07437, pp. 108\u2013130. Springer, Heidelberg (2012)"},{"doi-asserted-by":"crossref","unstructured":"Csallner, C., Xie, T.: DSD-Crasher: A hybrid analysis tool for bug finding. In: ISSTA (2006)","key":"16_CR10","DOI":"10.1145\/1146238.1146267"},{"key":"16_CR11","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 - a software analysis perspective. In: Eleftherakis, G., Hinchey, M., Holcombe, M. (eds.) SEFM 2012. LNCS, vol.\u00a07504, pp. 233\u2013247. Springer, Heidelberg (2012)"},{"doi-asserted-by":"crossref","unstructured":"Delahaye, M., Kosmatov, N., Signoles, J.: Common specification language for static and dynamic analysis of C programs. In: SAC (2013)","key":"16_CR12","DOI":"10.1145\/2480362.2480593"},{"key":"16_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"74","DOI":"10.1007\/978-3-642-02949-3_7","volume-title":"Tests and Proofs","author":"C. Gladisch","year":"2009","unstructured":"Gladisch, C.: Could we have chosen a better loop invariant or method contract? In: Dubois, C. (ed.) TAP 2009. LNCS, vol.\u00a05668, pp. 74\u201389. Springer, Heidelberg (2009)"},{"doi-asserted-by":"crossref","unstructured":"Godefroid, P., Nori, A.V., Rajamani, S.K., Tetali, S.D.: Compositional may-must program analysis: unleashing the power of alternation. In: POPL (2010)","key":"16_CR14","DOI":"10.1145\/1706299.1706307"},{"key":"16_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/978-3-642-17164-2_3","volume-title":"Programming Languages and Systems","author":"G. Klein","year":"2010","unstructured":"Klein, G.: From a verified kernel towards verified systems. In: Ueda, K. (ed.) APLAS 2010. LNCS, vol.\u00a06461, pp. 21\u201333. Springer, Heidelberg (2010)"},{"key":"16_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"262","DOI":"10.1007\/978-3-540-39656-7_11","volume-title":"Formal Methods for Components and Objects","author":"G.T. Leavens","year":"2003","unstructured":"Leavens, G.T., Cheon, Y., Clifton, C., Ruby, C., Cok, D.R.: How the design of JML accommodates both runtime assertion checking and formal verification. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2002. LNCS, vol.\u00a02852, pp. 262\u2013284. Springer, Heidelberg (2003)"},{"unstructured":"Petiot, G., Kosmatov, N., Giorgetti, A., Julliand, J.: StaDy: Deep Integration of Static and Dynamic Analysis in Frama-C. Tech. rep. (2014), \n                  \n                    http:\/\/hal.archives-ouvertes.fr\/hal-00992159","key":"16_CR17"},{"key":"16_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1007\/978-3-642-40787-1_15","volume-title":"Runtime Verification","author":"N. Polikarpova","year":"2013","unstructured":"Polikarpova, N., Furia, C.A., West, S.: To run what no one has run before: Executing an intermediate verification language. In: Legay, A., Bensalem, S. (eds.) RV 2013. LNCS, vol.\u00a08174, pp. 251\u2013268. Springer, Heidelberg (2013)"},{"unstructured":"Signoles, J.: E-ACSL: Executable ANSI\/ISO C Specification Language, \n                  \n                    http:\/\/frama-c.com\/download\/e-acsl\/e-acsl.pdf","key":"16_CR19"}],"container-title":["Lecture Notes in Computer Science","Tests and Proofs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-09099-3_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,27]],"date-time":"2019-05-27T02:31:35Z","timestamp":1558924295000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-09099-3_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319090986","9783319090993"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-09099-3_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}