{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,11]],"date-time":"2025-09-11T19:34:31Z","timestamp":1757619271431,"version":"3.44.0"},"publisher-location":"Cham","reference-count":32,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031986789"},{"type":"electronic","value":"9783031986796"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,7,22]],"date-time":"2025-07-22T00:00:00Z","timestamp":1753142400000},"content-version":"vor","delay-in-days":202,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>Statistical methods have been widely misused and misinterpreted in various scientific fields, raising significant concerns about the integrity of scientific research. To mitigate this problem, we propose a tool-assisted method for formally specifying and automatically verifying the correctness of statistical programs. In this method, programmers are required to annotate the source code of the statistical programs with the requirements for these methods. Through this annotation, they are reminded to check the requirements for statistical methods, including those that cannot be formally verified, such as the distribution of the unknown true population. Our software tool  automatically checks whether programmers have properly specified the requirements for the statistical methods, thereby identifying any missing requirements that need to be addressed. This tool is implemented using the Why3 platform to verify the correctness of OCaml programs that conduct statistical hypothesis testing. We demonstrate how  can be used to avoid common errors in various statistical hypothesis testing programs.<\/jats:p>","DOI":"10.1007\/978-3-031-98679-6_10","type":"book-chapter","created":{"date-parts":[[2025,7,21]],"date-time":"2025-07-21T09:20:37Z","timestamp":1753089637000},"page":"216-230","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["StatWhy: Formal Verification Tool for\u00a0Statistical Hypothesis Testing Programs"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2151-9560","authenticated-orcid":false,"given":"Yusuke","family":"Kawamoto","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0009-0004-3505-7151","authenticated-orcid":false,"given":"Kentaro","family":"Kobayashi","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7466-8789","authenticated-orcid":false,"given":"Kohei","family":"Suenaga","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,7,22]]},"reference":[{"key":"10_CR1","doi-asserted-by":"publisher","unstructured":"Ahrendt, W., Beckert, B., Bubel, R., H\u00e4hnle, R., Schmitt, P.H., Ulbrich, M.: Deductive Software Verification - The KeY Book - From Theory to Practice, Lecture Notes in Computer Science, vol. 10001. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-319-49812-6","DOI":"10.1007\/978-3-319-49812-6"},{"key":"10_CR2","doi-asserted-by":"publisher","unstructured":"Arbuthnot, J.: An argument for divine providence, taken from the constant regularity observ\u2019d in the births of both sexes. Philos. Trans. Roy. Soc. London 27(328), 186\u2013190 (1710). https:\/\/doi.org\/10.1098\/rstl.1710.0011","DOI":"10.1098\/rstl.1710.0011"},{"key":"10_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1007\/978-3-030-99524-9_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H Barbosa","year":"2022","unstructured":"Barbosa, H., et al.: cvc5: a versatile and industrial-strength SMT solver. In: TACAS 2022. LNCS, vol. 13243, pp. 415\u2013442. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_24"},{"key":"10_CR4","doi-asserted-by":"publisher","unstructured":"Bretz, F., Hothorn, T., Westfall, P.: Multiple Comparisons Using R. Chapman and Hall\/CRC (2010). https:\/\/doi.org\/10.1201\/9781420010909","DOI":"10.1201\/9781420010909"},{"key":"10_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"484","DOI":"10.1007\/978-3-030-30942-8_29","volume-title":"Formal Methods \u2013 The Next 30 Years","author":"A Chargu\u00e9raud","year":"2019","unstructured":"Chargu\u00e9raud, A., Filli\u00e2tre, J.-C., Louren\u00e7o, C., Pereira, M.: GOSPEL\u2014providing OCaml with a formal specification language. In: ter Beek, M.H., McIver, A., Oliveira, J.N. (eds.) FM 2019. LNCS, vol. 11800, pp. 484\u2013501. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-30942-8_29"},{"key":"10_CR6","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. 7504, pp. 233\u2013247. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-33826-7_16"},{"issue":"1","key":"10_CR7","doi-asserted-by":"publisher","first-page":"304","DOI":"10.1186\/1756-0500-4-304","volume":"4","author":"S Fernandes-Taylor","year":"2011","unstructured":"Fernandes-Taylor, S., Hyun, J.K., Reeder, R.N., Harris, A.H.: Common statistical and research design problems in manuscripts submitted to high-impact medical journals. BMC. Res. Notes 4(1), 304 (2011). https:\/\/doi.org\/10.1186\/1756-0500-4-304","journal-title":"BMC. Res. Notes"},{"key":"10_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/978-3-642-37036-6_8","volume-title":"Programming Languages and Systems","author":"J-C Filli\u00e2tre","year":"2013","unstructured":"Filli\u00e2tre, J.-C., Paskevich, A.: Why3 \u2014 where programs meet provers. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 125\u2013128. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-37036-6_8"},{"issue":"4S","key":"10_CR9","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1145\/2502508.2502520","volume":"48","author":"C Flanagan","year":"2013","unstructured":"Flanagan, C., Leino, K., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: PLDI 2002: extended static checking for Java. ACM SIGPLAN Not. 48(4S), 22\u201333 (2013). https:\/\/doi.org\/10.1145\/2502508.2502520","journal-title":"ACM SIGPLAN Not."},{"key":"10_CR10","doi-asserted-by":"publisher","unstructured":"Goldwasser, S., Rothblum, G.N., Shafer, J., Yehudayoff, A.: Interactive proofs for verifying machine learning. In: Lee, J.R. (ed.) Proceedings of the 12th Innovations in Theoretical Computer Science Conference (ITCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a0185, pp. 41:1\u201341:19. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2021). https:\/\/doi.org\/10.4230\/LIPIcs.ITCS.2021.41","DOI":"10.4230\/LIPIcs.ITCS.2021.41"},{"key":"10_CR11","unstructured":"Hogg, R.V., McKean, J.W., Craig, A.T.: Introduction to mathematical statistics. Pearson Education India (2013)"},{"key":"10_CR12","doi-asserted-by":"crossref","unstructured":"Kanji, G.K.: 100 Statistical Tests. Sage (2006)","DOI":"10.4135\/9781849208499"},{"key":"10_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"344","DOI":"10.1007\/978-3-030-31175-9_20","volume-title":"The Art of Modelling Computational Systems: A Journey from Logic and Concurrency to Security and Privacy","author":"Y Kawamoto","year":"2019","unstructured":"Kawamoto, Y.: Statistical epistemic logic. In: Alvim, M.S., Chatzikokolakis, K., Olarte, C., Valencia, F. (eds.) The Art of Modelling Computational Systems: A Journey from Logic and Concurrency to Security and Privacy. LNCS, vol. 11760, pp. 344\u2013362. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-31175-9_20"},{"key":"10_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1007\/978-3-030-30446-1_16","volume-title":"Software Engineering and Formal Methods","author":"Y Kawamoto","year":"2019","unstructured":"Kawamoto, Y.: Towards logical specification of statistical machine learning. In: \u00d6lveczky, P.C., Sala\u00fcn, G. (eds.) SEFM 2019. LNCS, vol. 11724, pp. 293\u2013311. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-30446-1_16"},{"issue":"2","key":"10_CR15","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1007\/s10270-020-00825-2","volume":"20","author":"Y Kawamoto","year":"2020","unstructured":"Kawamoto, Y.: An epistemic approach to the formal specification of statistical machine learning. Softw. Syst. Model. 20(2), 293\u2013310 (2020). https:\/\/doi.org\/10.1007\/s10270-020-00825-2","journal-title":"Softw. Syst. Model."},{"key":"10_CR16","unstructured":"Kawamoto, Y., Kobayashi, K., Suenaga, K.: User Documentation for StatWhy v.1.2 (2025). https:\/\/github.com\/fm4stats\/statwhy"},{"key":"10_CR17","doi-asserted-by":"publisher","unstructured":"Kawamoto, Y., Sato, T., Suenaga, K.: Formalizing statistical beliefs in hypothesis testing using program logic. In: Proceedings of KR 2021, pp. 411\u2013421 (2021). https:\/\/doi.org\/10.24963\/kr.2021\/39","DOI":"10.24963\/kr.2021\/39"},{"key":"10_CR18","doi-asserted-by":"publisher","unstructured":"Kawamoto, Y., Sato, T., Suenaga, K.: Formalizing statistical causality via modal logic. In: Proceedings of JELIA 2023. Lecture Notes in Computer Science, vol. 14281, pp. 681\u2013696. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-43619-2_46","DOI":"10.1007\/978-3-031-43619-2_46"},{"key":"10_CR19","doi-asserted-by":"publisher","DOI":"10.1016\/J.ARTINT.2023.104045","volume":"326","author":"Y Kawamoto","year":"2024","unstructured":"Kawamoto, Y., Sato, T., Suenaga, K.: Sound and relatively complete belief Hoare logic for statistical hypothesis testing programs. Artif. Intell. 326, 104045 (2024). https:\/\/doi.org\/10.1016\/J.ARTINT.2023.104045","journal-title":"Artif. Intell."},{"issue":"2","key":"10_CR20","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1016\/0022-0000(85)90012-1","volume":"30","author":"D Kozen","year":"1985","unstructured":"Kozen, D.: A probabilistic PDL. J. Comput. Syst. Sci. 30(2), 162\u2013178 (1985). https:\/\/doi.org\/10.1016\/0022-0000(85)90012-1","journal-title":"J. Comput. Syst. Sci."},{"key":"10_CR21","unstructured":"Leino, K.R.M.: This is Boogie 2. Manuscript KRML 178(131), 9 (2008)"},{"key":"10_CR22","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/978-3-642-17511-4_20","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"K Leino","year":"2010","unstructured":"Leino, K.: Dafny: an automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010. LNCS (LNAI), vol. 6355, pp. 348\u2013370. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-17511-4_20"},{"key":"10_CR23","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1016\/0167-9473(85)90057-X","volume":"3","author":"JP Lesage","year":"1985","unstructured":"Lesage, J.P., Simon, S.D.: Numerical accuracy of statistical algorithms for microcomputers. Comput. Stat. Data Anal. 3, 47\u201357 (1985). https:\/\/doi.org\/10.1016\/0167-9473(85)90057-X","journal-title":"Comput. Stat. Data Anal."},{"key":"10_CR24","doi-asserted-by":"publisher","DOI":"10.7554\/eLife.48175","volume":"8","author":"TR Makin","year":"2019","unstructured":"Makin, T.R., de Xivry, J.: Science forum: ten common statistical mistakes to watch out for when writing or reviewing a manuscript. Elife 8, e48175 (2019)","journal-title":"Elife"},{"issue":"1","key":"10_CR25","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1016\/j.ijsu.2011.10.001","volume":"10","author":"D Moher","year":"2012","unstructured":"Moher, D., et al.: Consort 2010 explanation and elaboration: updated guidelines for reporting parallel group randomised trials. Int. J. Surg. 10(1), 28\u201355 (2012)","journal-title":"Int. J. Surg."},{"issue":"3","key":"10_CR26","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1145\/229542.229547","volume":"18","author":"C Morgan","year":"1996","unstructured":"Morgan, C., McIver, A., Seidel, K.: Probabilistic predicate transformers. ACM Trans. Program. Lang. Syst. 18(3), 325\u2013353 (1996). https:\/\/doi.org\/10.1145\/229542.229547","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"10_CR27","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.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"10_CR28","unstructured":"Mutreja, S., Shafer, J.: Pac verification of statistical algorithms. In: Neu, G., Rosasco, L. (eds.) Proceedings of Thirty Sixth Conference on Learning Theory. Proceedings of Machine Learning Research, vol.\u00a0195, pp. 5021\u20135043. PMLR (2023)"},{"key":"10_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1007\/978-3-030-81688-9_31","volume-title":"Computer Aided Verification","author":"M Pereira","year":"2021","unstructured":"Pereira, M., Ravara, A.: Cameleer: a deductive verification tool for OCaml. In: Silva, A., Leino, K. (eds.) CAV 2021. LNCS, vol. 12760, pp. 677\u2013689. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81688-9_31"},{"issue":"7","key":"10_CR30","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1145\/3503914","volume":"65","author":"SA Seshia","year":"2022","unstructured":"Seshia, S.A., Sadigh, D., Sastry, S.S.: Toward verified artificial intelligence. Commun. ACM 65(7), 46\u201355 (2022). https:\/\/doi.org\/10.1145\/3503914","journal-title":"Commun. ACM"},{"key":"10_CR31","doi-asserted-by":"publisher","first-page":"867","DOI":"10.2471\/BLT.07.045120","volume":"85","author":"E Von Elm","year":"2007","unstructured":"Von Elm, E., Altman, D.G., Egger, M., Pocock, S.J., G\u00f8tzsche, P.C., Vandenbroucke, J.P.: The strengthening the reporting of observational studies in epidemiology (strobe) statement: guidelines for reporting observational studies. Bull. World Health Organ. 85, 867\u2013872 (2007)","journal-title":"Bull. World Health Organ."},{"issue":"2","key":"10_CR32","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1080\/00031305.2016.1154108","volume":"70","author":"RL Wasserstein","year":"2016","unstructured":"Wasserstein, R.L., Lazar, N.A.: The ASA statement on p-values: context, process, and purpose. Am. Stat. 70(2), 129\u2013133 (2016). https:\/\/doi.org\/10.1080\/00031305.2016.1154108","journal-title":"Am. Stat."}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-98679-6_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,7]],"date-time":"2025-09-07T16:17:52Z","timestamp":1757261872000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-98679-6_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031986789","9783031986796"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-98679-6_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"22 July 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Zagreb","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Croatia","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21 July 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 July 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"37","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conferences.i-cav.org\/2025\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}