{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,1]],"date-time":"2026-05-01T03:37:49Z","timestamp":1777606669974,"version":"3.51.4"},"reference-count":48,"publisher":"Association for Computing Machinery (ACM)","issue":"6","license":[{"start":{"date-parts":[[2018,11,1]],"date-time":"2018-11-01T00:00:00Z","timestamp":1541030400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2018,11]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>\n            Applying deductive verification to formally prove that a program respects its formal specification is a very complex and time-consuming task due in particular to the lack of feedback in case of proof failures. Along with a non-compliance between the code and its specification (due to an error in at least one of them), possible reasons of a proof failure include a missing or too weak specification for a called function or a loop, and lack of time or simply incapacity of the prover to finish a particular proof. This work proposes a methodology where test generation helps to identify the reason of a proof failure and to exhibit a counterexample clearly illustrating the issue. We define the categories of proof failures, introduce two subcategories of contract weaknesses (single and global ones), and examine their properties. We describe how to transform a C program formally specified in an executable specification language into C code suitable for testing, and illustrate the benefits of the method on comprehensive examples. The method has been implemented in\n            <jats:sc>StaDy<\/jats:sc>\n            , a plugin of the software analysis platform\n            <jats:sc>Frama<\/jats:sc>\n            -C. Initial experiments show that detecting non-compliances and contract weaknesses allows to precisely diagnose most proof failures.\n          <\/jats:p>","DOI":"10.1007\/s00165-018-0456-4","type":"journal-article","created":{"date-parts":[[2018,6,12]],"date-time":"2018-06-12T11:31:06Z","timestamp":1528803066000},"page":"629-657","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":14,"title":["How testing helps to diagnose proof failures"],"prefix":"10.1145","volume":"30","author":[{"given":"Guillaume","family":"Petiot","sequence":"first","affiliation":[{"name":"Software Reliability Laboratory, CEA, List, PC 174,  91191, Gif-sur-Yvette, France"},{"name":"FEMTO-ST Institute, University of Bourgogne Franche-Comt\u00e9, CNRS, 25030, Besan\u00e7on Cedex, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1557-2813","authenticated-orcid":false,"given":"Nikolai","family":"Kosmatov","sequence":"additional","affiliation":[{"name":"Software Reliability Laboratory, CEA, List, PC 174,  91191, Gif-sur-Yvette, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bernard","family":"Botella","sequence":"additional","affiliation":[{"name":"Software Reliability Laboratory, CEA, List, PC 174,  91191, Gif-sur-Yvette, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alain","family":"Giorgetti","sequence":"additional","affiliation":[{"name":"FEMTO-ST Institute, University of Bourgogne Franche-Comt\u00e9, CNRS, 25030, Besan\u00e7on Cedex, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jacques","family":"Julliand","sequence":"additional","affiliation":[{"name":"FEMTO-ST Institute, University of Bourgogne Franche-Comt\u00e9, CNRS, 25030, Besan\u00e7on Cedex, France"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","unstructured":"Arlt S Arenis SF Podelski A Wehrle M (2015) System testing and program verification. Softw Eng Manag vol 239 of LNI. GI pp 71\u201372"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"crossref","unstructured":"Ahn KY Denney E (2010) Testing first-order logic axioms in program verification. TAP vol 6143 of LNCS. Springer pp 22\u201337","DOI":"10.1007\/978-3-642-13977-2_4"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive theorem proving and program development; Coq\u2019Art: the calculus of inductive constructions Texts in theoretical computer science. An EATCS series","author":"Bertot Y.","year":"2004"},{"key":"e_1_2_1_2_4_2","unstructured":"Baudin P Cuoq P Filli\u00e2tre J-C March\u00e9 C. Monate B. Moy Y. Prevosto V (2017) ACSL: ANSI\/ISO C specification language. http:\/\/frama-c.com\/acsl.html"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"Botella B Delahaye M Hong Tuan Ha S Kosmatov N Mouy P Roger M Williams N (2009) Automating structural testing of C programs: experience with Path Crawler. AST. IEEE Computer Society pp 70\u201378","DOI":"10.1109\/IWAST.2009.5069043"},{"key":"e_1_2_1_2_6_2","unstructured":"Burghardt J Gerlach J (2017) ACSL by example. https:\/\/github.com\/fraunhoferfokus\/acsl-by-example"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"Beckert B H\u00e4hnle R Schmitt PH (eds) (2007) Verification of object-oriented software: the key approach.LNCS 4334. Springer Heidelberg","DOI":"10.1007\/978-3-540-69061-0"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","unstructured":"Blatter L. Kosmatov N. Le Gall P. Prevosto V. Petiot G. (2018) Static and dynamic verification of relational properties on self-composed C code. TAP LNCS. Springer To appear","DOI":"10.1007\/978-3-319-92994-1_3"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"crossref","unstructured":"Berghofer S Nipkow T (2004) Random testing in Isabelle\/HOL. SEFM. IEEE Computer Society pp 230\u2013239","DOI":"10.1109\/SEFM.2004.1347524"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"crossref","unstructured":"Cousot P Cousot R F\u00e4hndrich M Logozzo F (2013) Automatic inference of necessary preconditions. VMCAI vol 7737 of LNCS. Springer pp 128\u2013148","DOI":"10.1007\/978-3-642-35873-9_10"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.70.1"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"crossref","unstructured":"Christakis M Emmisberger P M\u00fcller P (2014) Dynamic 1075 test generation with static fields and initializers. RV vol 8734 of LNCS. Springer pp 269\u2013284","DOI":"10.1007\/978-3-319-11164-3_23"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"crossref","unstructured":"Christ J Ermis E Sch\u00e4f M Wies T (2013) Flow-sensitive fault localization. VMCAI vol 7737 of LNCS. Springer pp 189\u2013208","DOI":"10.1007\/978-3-642-35873-9_13"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"publisher","DOI":"10.1145\/876638.876643"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","unstructured":"Chebaro O Kosmatov N Giorgetti A Julliand J (2012) Program slicing enhances a verification technique combining static and dynamic analysis. SAC. ACM pp 1284\u20131291","DOI":"10.1145\/2245276.2231980"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"crossref","unstructured":"Christakis M Leino KRM M\u00fcller P W\u00fcstholz V. Integrated environment for diagnosing verification errors. TACAS vol 9636 of LNCS. Springer pp 424\u2013441","DOI":"10.1007\/978-3-662-49674-9_25"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","unstructured":"Christakis M M\u00fc ller P W\u00fcstholz V (2012) Collaborative verification and testing with explicit assumptions. FM vol 7436 of LNCS. Springer pp 132\u2013146","DOI":"10.1007\/978-3-642-32759-9_13"},{"key":"e_1_2_1_2_18_2","unstructured":"Coq Development Team. The Coq Proof Assistant Reference Manual 2018. http:\/\/coq.inria.fr\/."},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"crossref","unstructured":"Claessen K Svensson H (2008) Finding counter examples in induction proofs. TAP vol 4966 of LNCS. Springer pp 48\u201365","DOI":"10.1007\/978-3-540-79124-9_5"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2010.23"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"crossref","unstructured":"Dimitrova R Finkbeiner B (2012). Counterexample-guided synthesis of observation predicates. FORMATS vol 7595 of LNCS. Springer pp 107\u2013122","DOI":"10.1007\/978-3-642-33365-1_9"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"crossref","unstructured":"de Gouw S Rot J de Boer FS Bubel R H\u00e4hnle R (2015) Open JDK\u2019s Java.utils.Collection.sort() is broken: the good the bad and the worst case. CAV vol 9206 of LNCS. Springer pp 273\u2013289","DOI":"10.1007\/978-3-319-21690-4_16"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"crossref","unstructured":"Dybjer P Haiyan Q Takeyama M (2003) Combining testing and proving in dependent type theory. TPHOLs vol 2758 of LNCS. Springer pp 188\u2013203","DOI":"10.1007\/10930755_12"},{"key":"e_1_2_1_2_24_2","volume-title":"A discipline of programming Series in automatic computation","author":"Dijkstra EW.","year":"1976"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"crossref","unstructured":"Delahaye M Kosmatov N Signoles J (2013) Common specification language for static and dynamic analysis of C programs. SAC. ACM pp 1230\u20131235","DOI":"10.1145\/2480362.2480593"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"crossref","unstructured":"Engel C H\u00e4hnle R (2007) Generating unit tests from formal proofs. TAP vol 4454 of LNCS. Springer pp 169\u2013188","DOI":"10.1007\/978-3-540-73770-4_10"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"crossref","unstructured":"Genestier R Giorgetti A Petiot G (2015) Sequential generation of structured arrays and its deductive verification. TAP vol 9154 of LNCS. Springer pp 109\u2013128","DOI":"10.1007\/978-3-319-21215-9_7"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"crossref","unstructured":"Gulavani BS Henzinger TA Kannan Y Nori AV Rajamani SK (2006) SYNERGY: a new algorithm for property checking. FSE. ACM pp 117\u2013127","DOI":"10.1145\/1181775.1181790"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"crossref","unstructured":"Groce A Kroening D Lerda F (2004) Understanding counterexamples with explain. CAV vol 3114 of LNCS. Springer pp 453\u2013456","DOI":"10.1007\/978-3-540-27813-9_35"},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"crossref","unstructured":"Guo S Kusano M Wang C Yang Z Gupta A (2015) Assertion guided symbolic execution of multithreaded programs. ESEC\/FSE.ACM pp 854\u2013865","DOI":"10.1145\/2786805.2786841"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"crossref","unstructured":"Gladisch C (2009) Could we have chosen a better loop invariant or method contract?. TAP vol 5668 of LNCS. Springer pp 74\u201389","DOI":"10.1007\/978-3-642-02949-3_7"},{"key":"e_1_2_1_2_32_2","doi-asserted-by":"crossref","unstructured":"Godefroid P Nori AV Rajamani SK Tetali SD (2010) Compositional may-must program analysis: unleashing the power of alternation. POPL. ACM pp 43\u201356","DOI":"10.1145\/1707801.1706307"},{"key":"e_1_2_1_2_33_2","doi-asserted-by":"crossref","unstructured":"Hauzar D March\u00e9 C Moy Y (2016) Counterexamples from proof failures in SPARK. SEFM vol 9763 of LNCS . Springer pp 215\u2013233","DOI":"10.1007\/978-3-319-41591-8_15"},{"key":"e_1_2_1_2_34_2","doi-asserted-by":"crossref","unstructured":"Jakobsson A Kosmatov N Signoles J (2015) Fast as a shadow expressive as a tree: hybrid memory monitoring for C. SAC. ACM pp 1765\u20131772","DOI":"10.1145\/2695664.2695815"},{"key":"e_1_2_1_2_35_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-014-0326-7"},{"key":"e_1_2_1_2_36_2","unstructured":"Kosmatov N (2010\u20132015). Online version of PathCrawler.http:\/\/pathcrawler-online.com\/"},{"key":"e_1_2_1_2_37_2","doi-asserted-by":"crossref","unstructured":"Kosmatov N. Petiot G. Signoles J. (2013) An optimized memory monitoring for runtime assertion checking of C programs. RV vol 8174 of LNCS . Springer pp 328\u2013333","DOI":"10.1007\/978-3-642-40787-1_10"},{"key":"e_1_2_1_2_38_2","doi-asserted-by":"crossref","unstructured":"Kov\u00e1cs L Voronkov A (2009) Finding loop invariants for programs over arrays using a theorem prover. FASE vol 5503 of LNCS. Springer pp 470\u2013485","DOI":"10.1007\/978-3-642-00593-0_33"},{"key":"e_1_2_1_2_39_2","doi-asserted-by":"crossref","unstructured":"M\u00fcller P Ruskiewicz JN (2011) Using debuggers to understand failed verification attempts. FM vol 6664 of LNCS. Springer pp 73\u201387","DOI":"10.1007\/978-3-642-21437-0_8"},{"key":"e_1_2_1_2_40_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipl.2013.05.008"},{"key":"e_1_2_1_2_41_2","unstructured":"Owre S (2006) Random testing in PVS. Workshop on automated formal methods (AFM)"},{"key":"e_1_2_1_2_42_2","doi-asserted-by":"crossref","unstructured":"Petiot G Botella B Julliand J Kosmatov N Signoles J (2014) Instrumentation of annotated C programs for test generation. SCAM. IEEE Computer Society pp 105\u2013114","DOI":"10.1109\/SCAM.2014.19"},{"key":"e_1_2_1_2_43_2","doi-asserted-by":"crossref","unstructured":"Petiot G Kosmatov N Botella B Giorgetti A Julliand J (2016) Your proof fails? Testing helps to find the reason. TAP vol 9762 of LNCS. Springer pp 130\u2013150","DOI":"10.1007\/978-3-319-41135-4_8"},{"key":"e_1_2_1_2_44_2","doi-asserted-by":"crossref","unstructured":"Petiot G Kosmatov N Giorgetti A Julliand J (2014) Howtest generation helps software specification and deductive verification in Frama-C. TAP vol 8570 of LNCS. Springer pp 53\u201360","DOI":"10.1007\/978-3-319-09099-3_16"},{"key":"e_1_2_1_2_45_2","doi-asserted-by":"crossref","unstructured":"Podelski A Wies T (2010) Counterexample-guided focus. POPL. ACM pp 249\u2013260","DOI":"10.1145\/1707801.1706330"},{"key":"e_1_2_1_2_46_2","unstructured":"Signoles J (2012). E-ACSL: executable ANSI\/ISO C specification language. http:\/\/frama-c.com\/download\/e-acsl\/e-acsl.pdf."},{"key":"e_1_2_1_2_47_2","doi-asserted-by":"crossref","unstructured":"Tschannen J Furia CA Nordio M Meyer B(2013) Program checking with less hassle. VSTTE vol 8164 of LNCS. Springer pp 149\u2013169","DOI":"10.1007\/978-3-642-54108-7_8"},{"key":"e_1_2_1_2_48_2","doi-asserted-by":"crossref","unstructured":"Williams N Marre B Mouy P Roger M (2005) PathCrawler: automatic generation of path tests by combining static and dynamic analysis. EDCC vol 3463 LNCS. Springer pp 281\u2013292","DOI":"10.1007\/11408901_21"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-018-0456-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-018-0456-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-018-0456-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-018-0456-4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T16:20:38Z","timestamp":1641486038000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-018-0456-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,11]]},"references-count":48,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2018,11]]}},"alternative-id":["10.1007\/s00165-018-0456-4"],"URL":"https:\/\/doi.org\/10.1007\/s00165-018-0456-4","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,11]]},"assertion":[{"value":"23 June 2017","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"18 April 2018","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"12 June 2018","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}