{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T12:00:34Z","timestamp":1770292834451,"version":"3.49.0"},"publisher-location":"Cham","reference-count":43,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319411347","type":"print"},{"value":"9783319411354","type":"electronic"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-41135-4_8","type":"book-chapter","created":{"date-parts":[[2016,6,20]],"date-time":"2016-06-20T12:23:38Z","timestamp":1466425418000},"page":"130-150","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":16,"title":["Your Proof Fails? Testing Helps to Find the Reason"],"prefix":"10.1007","author":[{"given":"Guillaume","family":"Petiot","sequence":"first","affiliation":[]},{"given":"Nikolai","family":"Kosmatov","sequence":"additional","affiliation":[]},{"given":"Bernard","family":"Botella","sequence":"additional","affiliation":[]},{"given":"Alain","family":"Giorgetti","sequence":"additional","affiliation":[]},{"given":"Jacques","family":"Julliand","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,6,21]]},"reference":[{"key":"8_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":"KY 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. 6143, pp. 22\u201337. Springer, Heidelberg (2010)"},{"key":"8_CR2","unstructured":"Arlt, S., Arenis, S.F., Podelski, A., Wehrle, M.: System testing and program verification. In: Software Engineering & Management (2015)"},{"key":"8_CR3","unstructured":"Arndt, J.: Matters Computational-Ideas, Algorithms, Source Code [The fxtbook] (2010). \n                      http:\/\/www.jjj.de"},{"key":"8_CR4","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                      http:\/\/frama-c.com\/acsl.html"},{"key":"8_CR5","unstructured":"Berghofer, S., Nipkow, T.: Random testing in Isabelle\/HOL. In: SEFM (2004)"},{"key":"8_CR6","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)","DOI":"10.1109\/IWAST.2009.5069043"},{"key":"8_CR7","unstructured":"Burghardt, J., Gerlach, J., Lapawczyk, T.: ACSL by Example (2016). \n                      https:\/\/gitlab.fokus.fraunhofer.de\/verification\/open-acslbyexample\/blob\/master\/ACSL-by-Example.pdf"},{"key":"8_CR8","doi-asserted-by":"crossref","unstructured":"Chamarthi, H.R., Dillinger, P.C., Kaufmann, M., Manolios, P.: Integrating testing and interactive theorem proving. In: ACL2 (2011)","DOI":"10.4204\/EPTCS.70.1"},{"key":"8_CR9","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)","DOI":"10.1145\/2245276.2231980"},{"key":"8_CR10","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1109\/TSE.2010.23","volume":"37","author":"TY Chen","year":"2011","unstructured":"Chen, T.Y., Tse, T.H., Zhou, Z.Q.: Semi-proving: an integrated method for program proving, testing, and debugging. IEEE Trans. Softw. Eng. 37, 109 (2011)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"8_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1007\/978-3-642-35873-9_13","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"J Christ","year":"2013","unstructured":"Christ, J., Ermis, E., Sch\u00e4f, M., Wies, T.: Flow-sensitive fault localization. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 189\u2013208. Springer, Heidelberg (2013)"},{"key":"8_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"424","DOI":"10.1007\/978-3-662-49674-9_25","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M Christakis","year":"2016","unstructured":"Christakis, M., Leino, K.R.M., M\u00fcller, P., W\u00fcstholz, V.: Integrated environment for diagnosing verification errors. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 424\u2013441. Springer, Heidelberg (2016). doi:\n                      10.1007\/978-3-662-49674-9_25"},{"key":"8_CR13","doi-asserted-by":"crossref","unstructured":"Christakis, M., Emmisberger, P., M\u00fcller, P.: Dynamic test generation with static fields and initializers. In: RV (2014)","DOI":"10.1007\/978-3-319-11164-3_23"},{"key":"8_CR14","doi-asserted-by":"crossref","unstructured":"Christakis, M., M\u00fcller, P., W\u00fcstholz, V.: Collaborative verification and testing with explicit assumptions. In: FM (2012)","DOI":"10.1007\/978-3-642-32759-9_13"},{"key":"8_CR15","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. 4966, pp. 48\u201365. Springer, Heidelberg (2008)"},{"key":"8_CR16","doi-asserted-by":"publisher","first-page":"752","DOI":"10.1145\/876638.876643","volume":"50","author":"E Clarke","year":"2003","unstructured":"Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. J. ACM 50, 752 (2003)","journal-title":"J. ACM"},{"key":"8_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1007\/978-3-642-35873-9_10","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"P Cousot","year":"2013","unstructured":"Cousot, P., Cousot, R., F\u00e4hndrich, M., Logozzo, F.: Automatic inference of necessary preconditions. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 128\u2013148. Springer, Heidelberg (2013)"},{"key":"8_CR18","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)","DOI":"10.1145\/2480362.2480593"},{"key":"8_CR19","series-title":"Series in Automatic Computation","volume-title":"A Discipline of Programming","author":"EW Dijkstra","year":"1976","unstructured":"Dijkstra, E.W.: A Discipline of Programming. Series in Automatic Computation. Prentice Hall, Englewood Cliffs (1976)"},{"key":"8_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/978-3-642-33365-1_9","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"R Dimitrova","year":"2012","unstructured":"Dimitrova, R., Finkbeiner, B.: Counterexample-guided synthesis of observation predicates. In: Jurdzi\u0144ski, M., Ni\u010dkovi\u0107, D. (eds.) FORMATS 2012. LNCS, vol. 7595, pp. 107\u2013122. Springer, Heidelberg (2012)"},{"key":"8_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1007\/10930755_12","volume-title":"Theorem Proving in Higher Order Logics","author":"P Dybjer","year":"2003","unstructured":"Dybjer, P., Haiyan, Q., Takeyama, M.: Combining testing and proving in dependent type theory. In: Basin, D., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol. 2758, pp. 188\u2013203. Springer, Heidelberg (2003)"},{"key":"8_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1007\/978-3-540-73770-4_10","volume-title":"Tests and Proofs","author":"C Engel","year":"2007","unstructured":"Engel, C., H\u00e4hnle, R.: Generating unit tests from formal proofs. In: Gurevich, Y., Meyer, B. (eds.) TAP 2007. LNCS, vol. 4454, pp. 169\u2013188. Springer, Heidelberg (2007)"},{"key":"8_CR23","series-title":"lecture notes in computer science","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1007\/978-3-319-21215-9_7","volume-title":"Tests and Proofs","author":"R Genestier","year":"2015","unstructured":"Genestier, R., Giorgetti, A., Petiot, G.: Sequential generation of structured arrays and its deductive verification. In: Blanchette, J.C., Kosmatov, N. (eds.) TAP 2015. LNCS, vol. 9154, pp. 109\u2013128. Springer, Heidelberg (2015)"},{"key":"8_CR24","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. 5668, pp. 74\u201389. Springer, Heidelberg (2009)"},{"key":"8_CR25","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)","DOI":"10.1145\/1706299.1706307"},{"key":"8_CR26","doi-asserted-by":"crossref","unstructured":"Groce, A., Kroening, D., Lerda, F.: Understanding counterexamples with explain. In: CAV (2004)","DOI":"10.1007\/978-3-540-27813-9_35"},{"key":"8_CR27","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: FSE (2006)","DOI":"10.1145\/1181775.1181790"},{"key":"8_CR28","doi-asserted-by":"crossref","unstructured":"Guo, S., Kusano, M., Wang, C., Yang, Z., Gupta, A.: Assertion guided symbolic execution of multithreaded programs. In: ESEC\/FSE (2015)","DOI":"10.1145\/2786805.2786841"},{"key":"8_CR29","unstructured":"Hauzar, D., March\u00e9, C., Moy, Y.: Counterexamples from proof failures in SPARK. In: SEFM (to appear, 2016)"},{"key":"8_CR30","doi-asserted-by":"crossref","unstructured":"Jakobsson, A., Kosmatov, N., Signoles, J.: Fast as a shadow, expressive as a tree: hybrid memory monitoring for C. In: SAC (2015)","DOI":"10.1145\/2695664.2695815"},{"issue":"3","key":"8_CR31","doi-asserted-by":"publisher","first-page":"573","DOI":"10.1007\/s00165-014-0326-7","volume":"27","author":"F Kirchner","year":"2015","unstructured":"Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C: a software analysis perspective. Formal Asp. Comput. 27(3), 573\u2013609 (2015). \n                      http:\/\/frama-c.com","journal-title":"Formal Asp. Comput."},{"key":"8_CR32","unstructured":"Kosmatov, N.: Online version of PathCrawler (2010\u20132015). \n                      http:\/\/pathcrawler-online.com\/"},{"key":"8_CR33","doi-asserted-by":"crossref","unstructured":"Kosmatov, N., Petiot, G., Signoles, J.: An optimized memory monitoring for runtime assertion checking of C programs. In: RV (2013)","DOI":"10.1007\/978-3-642-40787-1_10"},{"key":"8_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"470","DOI":"10.1007\/978-3-642-00593-0_33","volume-title":"Fundamental Approaches to Software Engineering","author":"L Kov\u00e1cs","year":"2009","unstructured":"Kov\u00e1cs, L., Voronkov, A.: Finding loop invariants for programs over arrays using a theorem prover. In: Chechik, M., Wirsing, M. (eds.) FASE 2009. LNCS, vol. 5503, pp. 470\u2013485. Springer, Heidelberg (2009)"},{"key":"8_CR35","doi-asserted-by":"crossref","unstructured":"M\u00fcller, P., Ruskiewicz, J.N.: Using debuggers to understand failed verification attempts. In: FM (2011)","DOI":"10.1007\/978-3-642-21437-0_8"},{"key":"8_CR36","unstructured":"Owre, S.: Random testing in PVS. In: AFM (2006)"},{"key":"8_CR37","doi-asserted-by":"crossref","unstructured":"Petiot, G., Botella, B., Julliand, J., Kosmatov, N., Signoles, J.: Instrumentation of annotated C programs for test generation. In: SCAM (2014)","DOI":"10.1109\/SCAM.2014.19"},{"key":"8_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"204","DOI":"10.1007\/978-3-319-09099-3_16","volume-title":"Tests and Proofs","author":"G Petiot","year":"2014","unstructured":"Petiot, G., Kosmatov, N., Giorgetti, A., Julliand, J.: How test generation helps software specification and deductive verification in Frama-C. In: Seidl, M., Tillmann, N. (eds.) TAP 2014. LNCS, vol. 8570, pp. 204\u2013211. Springer, Heidelberg (2014)"},{"key":"8_CR39","doi-asserted-by":"crossref","unstructured":"Podelski, A., Wies, T.: Counterexample-guided focus. In: POPL (2010)","DOI":"10.1145\/1706299.1706330"},{"key":"8_CR40","unstructured":"Signoles, J.: E-ACSL: Executable ANSI\/ISO C Specification Language. \n                      http:\/\/frama-c.com\/download\/e-acsl\/e-acsl.pdf"},{"key":"8_CR41","unstructured":"The Coq Development Team: The Coq proof assistant. \n                      http:\/\/coq.inria.fr"},{"key":"8_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/978-3-642-54108-7_8","volume-title":"Verified Software: Theories, Tools, Experiments","author":"J Tschannen","year":"2014","unstructured":"Tschannen, J., Furia, C.A., Nordio, M., Meyer, B.: Program checking with less hassle. In: Cohen, E., Rybalchenko, A. (eds.) VSTTE 2013. LNCS, vol. 8164, pp. 149\u2013169. Springer, Heidelberg (2014)"},{"key":"8_CR43","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","Tests and Proofs"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-41135-4_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,20]],"date-time":"2019-05-20T00:49:35Z","timestamp":1558313375000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-41135-4_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319411347","9783319411354"],"references-count":43,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-41135-4_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"21 June 2016","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}