{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T12:48:56Z","timestamp":1742993336826,"version":"3.40.3"},"publisher-location":"Cham","reference-count":25,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031781155"},{"type":"electronic","value":"9783031781162"}],"license":[{"start":{"date-parts":[[2024,11,29]],"date-time":"2024-11-29T00:00:00Z","timestamp":1732838400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,11,29]],"date-time":"2024-11-29T00:00:00Z","timestamp":1732838400000},"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":[[2025]]},"DOI":"10.1007\/978-3-031-78116-2_9","type":"book-chapter","created":{"date-parts":[[2024,11,28]],"date-time":"2024-11-28T07:31:08Z","timestamp":1732779068000},"page":"139-152","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Formally Verified Implementation of\u00a0the\u00a0K-Nearest Neighbors Classification Algorithm"],"prefix":"10.1007","author":[{"given":"Bernny","family":"Velasquez","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jessica","family":"Herring","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0004-0927-4355","authenticated-orcid":false,"given":"Nadeem Abdul","family":"Hamid","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,11,29]]},"reference":[{"key":"9_CR1","unstructured":"The Coq proof assistant, v8.16 (2022). https:\/\/coq.inria.fr\/"},{"key":"9_CR2","doi-asserted-by":"crossref","unstructured":"Anderson, E.: The species problem in Iris. Ann. Mo. Bot. Gard. 23(3), 457\u2013509 (1936). http:\/\/www.jstor.org\/stable\/2394164","DOI":"10.2307\/2394164"},{"key":"9_CR3","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-19718-5_1","volume-title":"Programming Languages and Systems","author":"AW Appel","year":"2011","unstructured":"Appel, A.W.: Verified software toolchain. In: Barthe, G. (ed.) Programming Languages and Systems, pp. 1\u201317. Springer, Berlin Heidelberg, Berlin, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-19718-5_1"},{"key":"9_CR4","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1007\/11737414_9","volume-title":"Functional and Logic Programming","author":"G Barthe","year":"2006","unstructured":"Barthe, G., Forest, J., Pichardie, D., Rusu, V.: Defining and reasoning about recursive functions: a practical tool for the coq proof assistant. In: Hagiya, M., Wadler, P. (eds.) Functional and Logic Programming, pp. 114\u2013129. Springer, Berlin Heidelberg, Berlin, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11737414_9"},{"key":"9_CR5","doi-asserted-by":"publisher","unstructured":"Barthe, G., Gr\u00e9goire, B., Zanella\u00a0B\u00e9guelin, S.: Formal certification of code-based cryptographic proofs. In: POPL \u201909: Proceedings of the 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 90\u2013101. Association for Computing Machinery, New York, NY, USA (2009). https:\/\/doi.org\/10.1145\/1480881.1480894","DOI":"10.1145\/1480881.1480894"},{"issue":"9","key":"9_CR6","doi-asserted-by":"publisher","first-page":"509","DOI":"10.1145\/361002.361007","volume":"18","author":"JL Bentley","year":"1975","unstructured":"Bentley, J.L.: Multidimensional binary search trees used for associative searching. Commun. ACM 18(9), 509\u2013517 (1975). https:\/\/doi.org\/10.1145\/361002.361007","journal-title":"Commun. ACM"},{"key":"9_CR7","doi-asserted-by":"publisher","unstructured":"Bertot, Y., Castran, P.: Interactive Theorem Proving and Program Development: Coq\u2019Art The Calculus of Inductive Constructions. Springer Publishing Company, 1st edn. (2010). https:\/\/doi.org\/10.1007\/978-3-662-07964-5","DOI":"10.1007\/978-3-662-07964-5"},{"key":"9_CR8","doi-asserted-by":"publisher","first-page":"110542","DOI":"10.1016\/j.jss.2020.110542","volume":"164","author":"HB Braiek","year":"2020","unstructured":"Braiek, H.B., Khomh, F.: On testing machine learning programs. J. Syst. Softw. 164, 110542 (2020). https:\/\/doi.org\/10.1016\/j.jss.2020.110542","journal-title":"J. Syst. Softw."},{"issue":"1","key":"9_CR9","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1109\/TIT.1967.1053964","volume":"13","author":"T Cover","year":"1967","unstructured":"Cover, T., Hart, P.: Nearest neighbor pattern classification. IEEE Trans. Inf. Theory 13(1), 21\u201327 (1967). https:\/\/doi.org\/10.1109\/TIT.1967.1053964","journal-title":"IEEE Trans. Inf. Theory"},{"key":"9_CR10","doi-asserted-by":"publisher","unstructured":"Cunningham, P., Delany, S.J.: K-nearest neighbour classifiers - a tutorial. ACM Comput. Surv. 54(6), 1\u201325 (2021). https:\/\/doi.org\/10.1145\/3459665","DOI":"10.1145\/3459665"},{"key":"9_CR11","doi-asserted-by":"publisher","unstructured":"Fan, A.Z., Koutris, P.: Certifiable robustness for nearest neighbor classifiers. In: Olteanu, D., Vortmeier, N. (eds.) 25th International Conference on Database Theory, ICDT 2022, March 29 to April 1, 2022, Edinburgh, UK (Virtual Conference). LIPIcs, vol.\u00a0220, pp. 1\u201320. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2022). https:\/\/doi.org\/10.4230\/LIPICS.ICDT.2022.6","DOI":"10.4230\/LIPICS.ICDT.2022.6"},{"key":"9_CR12","doi-asserted-by":"crossref","unstructured":"Fassina, N., Ranzato, F., Zanella, M.: Robustness certification of k-nearest neighbors. In: Proceedings of the 23rd IEEE International Conference on Data Mining (ICDM\u201923) (2023)","DOI":"10.1109\/ICDM58522.2023.00020"},{"issue":"3","key":"9_CR13","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1145\/355744.355745","volume":"3","author":"JH Friedman","year":"1977","unstructured":"Friedman, J.H., Bentley, J.L., Finkel, R.A.: An algorithm for finding best matches in logarithmic expected time. ACM Trans. Math. Softw. 3(3), 209\u2013226 (1977). https:\/\/doi.org\/10.1145\/355744.355745","journal-title":"ACM Trans. Math. Softw."},{"key":"9_CR14","unstructured":"Gu, R., Shao, Z., Chen, H., Wu, X., Kim, J., Sj\u00f6berg, V., Costanzo, D.: Certikos: an extensible architecture for building certified concurrent OS kernels. In: OSDI\u201916: Proceedings of the 12th USENIX Conference on Operating Systems Design and Implementation, pp. 653\u2013669. USENIX Association, USA (2016)"},{"issue":"5","key":"9_CR15","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1109\/52.57887","volume":"7","author":"JA Hall","year":"1990","unstructured":"Hall, J.A.: Seven myths of formal methods. IEEE Softw. 7(5), 11\u201319 (1990)","journal-title":"IEEE Softw."},{"key":"9_CR16","doi-asserted-by":"publisher","unstructured":"Hamid, N.A.: (Nearest) neighbors you can rely on: formally verified k-d tree construction and search in Coq. In: SAC \u201924: Proceedings of the 39th ACM\/SIGAPP Symposium on Applied Computing, pp. 1684\u20131693. Association for Computing Machinery, New York, NY, USA (2024). https:\/\/doi.org\/10.1145\/3605098.3635960","DOI":"10.1145\/3605098.3635960"},{"issue":"4","key":"9_CR17","doi-asserted-by":"publisher","first-page":"379","DOI":"10.1007\/BF01211297","volume":"9","author":"R Kneuper","year":"1997","unstructured":"Kneuper, R.: Limits of formal methods. Form. Asp. Comput. 9(4), 379\u2013394 (1997). https:\/\/doi.org\/10.1007\/BF01211297","journal-title":"Form. Asp. Comput."},{"issue":"7","key":"9_CR18","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X Leroy","year":"2009","unstructured":"Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107\u2013115 (2009). https:\/\/doi.org\/10.1145\/1538788.1538814","journal-title":"Commun. ACM"},{"key":"9_CR19","doi-asserted-by":"publisher","unstructured":"Luckcuck, M., Farrell, M., Dennis, L.A., Dixon, C., Fisher, M.: Formal specification and verification of autonomous robotic systems: a survey. ACM Comput. Surv. 52(5), 1\u201341 (2019). https:\/\/doi.org\/10.1145\/3342355","DOI":"10.1145\/3342355"},{"issue":"05","key":"9_CR20","first-page":"30","volume":"10","author":"D Namiot","year":"2022","unstructured":"Namiot, D., Ilyushin, E., Chizhov, I.: On a formal verification of machine learning systems. Int. J. Open Inf. Technol. 10(05), 30\u201334 (2022)","journal-title":"Int. J. Open Inf. Technol."},{"key":"9_CR21","unstructured":"Pierce, B.C., et al.: Logical Foundations, Software Foundations, vol.\u00a01. Electronic textbook (2023). http:\/\/softwarefoundations.cis.upenn.edu, version 6.5"},{"key":"9_CR22","unstructured":"Selsam, D., Liang, P., Dill, D.L.: Developing bug-free machine learning systems with formal mathematics. In: ICML\u201917: Proceedings of the 34th International Conference on Machine Learning, vol. 70, pp. 3047\u20133056. JMLR.org (2017)"},{"issue":"7","key":"9_CR23","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":"9_CR24","volume-title":"Advances in Neural Information Processing Systems","author":"C Sitawarin","year":"2021","unstructured":"Sitawarin, C., Kornaropoulos, E.M., Song, D., Wagner, D.: Adversarial examples for k-nearest neighbor classifiers based on higher-order voronoi diagrams. In: Beygelzimer, A., Dauphin, Y., Liang, P., Vaughan, J.W. (eds.) Advances in Neural Information Processing Systems, vol. 34. Curran Associates Inc, Red Hook, NY (2021)"},{"key":"9_CR25","doi-asserted-by":"publisher","unstructured":"Syriopoulos, P.K., Kalampalikis, N.G., Kotsiantis, S.B., Vrahatis, M.N.: kNN classification: a review. Ann. Math. Artif. Intell. 1\u201333 (2023). https:\/\/doi.org\/10.1007\/s10472-023-09882-x","DOI":"10.1007\/s10472-023-09882-x"}],"container-title":["Lecture Notes in Computer Science","Formal Methods: Foundations and Applications"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-78116-2_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,28]],"date-time":"2024-11-28T09:04:29Z","timestamp":1732784669000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-78116-2_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,11,29]]},"ISBN":["9783031781155","9783031781162"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-78116-2_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024,11,29]]},"assertion":[{"value":"29 November 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SBMF","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Brazilian Symposium on Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Vit\u00f3ria","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Brazil","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 December 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"5 December 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"sbmf2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}