{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,12]],"date-time":"2025-11-12T13:27:08Z","timestamp":1762954028432,"version":"3.41.0"},"reference-count":49,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2025,1,22]],"date-time":"2025-01-22T00:00:00Z","timestamp":1737504000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"DARPA","award":["HR001120C0159"],"award-info":[{"award-number":["HR001120C0159"]}]},{"name":"NSF DCCF","award":["SHF-1918429 and CCS-2140207"],"award-info":[{"award-number":["SHF-1918429 and CCS-2140207"]}]},{"name":"US DoD","award":["W911NF2010310"],"award-info":[{"award-number":["W911NF2010310"]}]},{"name":"DPI-Univ. of Illinois","award":["DPI-Univ. of Illinois"],"award-info":[{"award-number":["DPI-Univ. of Illinois"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Commun. ACM"],"published-print":{"date-parts":[[2025,2]]},"abstract":"<jats:p>Self-certification is an alternative to daunting verification or capricious testing, designed to produce a correctness justification that can be validated easily and independently.<\/jats:p>","DOI":"10.1145\/3689624","type":"journal-article","created":{"date-parts":[[2025,1,13]],"date-time":"2025-01-13T19:11:32Z","timestamp":1736795492000},"page":"74-84","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Program Correctness through Self-Certification"],"prefix":"10.1145","volume":"68","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6379-2442","authenticated-orcid":false,"given":"Kedar S.","family":"Namjoshi","sequence":"first","affiliation":[{"name":"Nokia Bell Labs, Murray Hill, New Jersey, United States"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3613-1208","authenticated-orcid":false,"given":"Lenore D.","family":"Zuck","sequence":"additional","affiliation":[{"name":"University of Illinois Chicago, Chicago, Illinois, United States"}]}],"member":"320","published-online":{"date-parts":[[2025,1,22]]},"reference":[{"key":"e_1_3_1_2_2","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_20"},{"key":"e_1_3_1_3_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40084-1_6"},{"key":"e_1_3_1_4_2","doi-asserted-by":"publisher","DOI":"10.1145\/3477579"},{"key":"e_1_3_1_5_2","volume-title":"Technical Report TR-88-009","author":"Blum M.","year":"1988","unstructured":"Blum, M. Designing programs to check their work. Technical Report TR-88-009, Intern. Computer Science Institute, UCB (1988)."},{"key":"e_1_3_1_6_2","doi-asserted-by":"publisher","DOI":"10.1145\/73007.73015"},{"key":"e_1_3_1_7_2","doi-asserted-by":"publisher","DOI":"10.1145\/200836.200880"},{"key":"e_1_3_1_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-84628-970-5"},{"key":"e_1_3_1_9_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-63166-6_21"},{"key":"e_1_3_1_10_2","doi-asserted-by":"publisher","DOI":"10.1007\/BFB0025774"},{"key":"e_1_3_1_11_2","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_3_1_12_2","unstructured":"Dijkstra E.W. On the reliability of programs. (1971);\u00a0https:\/\/wapo.st\/4gskw7y"},{"key":"e_1_3_1_13_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-56922-7_32"},{"key":"e_1_3_1_14_2","unstructured":"Euclid. Elements VII ([n.d.]);\u00a0https:\/\/bit.ly\/49T5XHz"},{"key":"e_1_3_1_15_2","first-page":"43","volume-title":"Complexity of Computation: Proceedings of the Symp. in Applied Mathematics of the American Mathematical Society and the Society for Industrial and Applied 7","author":"Fagin R.","year":"1973","unstructured":"Fagin, R. Generalized first-order spectra and polynomial-time recognizable sets. In Complexity of Computation: Proceedings of the Symp. in Applied Mathematics of the American Mathematical Society and the Society for Industrial and Applied 7, R.M. Karp (Ed.). American Mathematical Society (1973), 43\u201373."},{"key":"e_1_3_1_16_2","doi-asserted-by":"publisher","DOI":"10.46298\/DMTCS.6280"},{"key":"e_1_3_1_17_2","doi-asserted-by":"publisher","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"e_1_3_1_18_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-46002-0_24"},{"key":"e_1_3_1_19_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38574-2_24"},{"key":"e_1_3_1_20_2","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_3_1_21_2","doi-asserted-by":"publisher","DOI":"10.5555\/3921"},{"key":"e_1_3_1_22_2","doi-asserted-by":"publisher","DOI":"10.1145\/1073814.1073817"},{"key":"e_1_3_1_23_2","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_3_1_24_2","doi-asserted-by":"publisher","DOI":"10.1137\/0215074"},{"key":"e_1_3_1_25_2","volume-title":"Distributed Algorithms","author":"Lynch N.A.","year":"1996","unstructured":"Lynch, N.A. Distributed Algorithms. Morgan Kaufmann (1996)."},{"key":"e_1_3_1_26_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-09510-1_31"},{"key":"e_1_3_1_27_2","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(84)90003-0"},{"key":"e_1_3_1_28_2","first-page":"33","volume-title":"Proceedings of Symp. in Applied Mathematics 19","author":"McCarthy J.","year":"1967","unstructured":"McCarthy, J. and Painter, J. Correctness of a compiler for arithmetical expressions. In Proceedings of Symp. in Applied Mathematics 19, Mathematical Aspects of Computer Science (1967), 33\u201341."},{"key":"e_1_3_1_29_2","doi-asserted-by":"publisher","DOI":"10.1016\/J.COSREV.2010.09.009"},{"key":"e_1_3_1_30_2","unstructured":"McMillan K.L. Ivy; http:\/\/microsoft.github.io\/ivy."},{"key":"e_1_3_1_31_2","first-page":"481","volume-title":"Proceedings of the 2nd Intern. Joint Conf. on Artificial Intelligence","author":"Milner R.","year":"1971","unstructured":"Milner, R. An algebraic definition of simulation between programs. In Proceedings of the 2nd Intern. Joint Conf. on Artificial Intelligence, D.C. Cooper (Ed.). W. Kaufmann (Sept. 1971), 481\u2013489; http:\/\/ijcai.org\/Proceedings\/71\/Papers\/044.pdf"},{"key":"e_1_3_1_32_2","volume-title":"Communication and Concurrency","author":"Milner R.","year":"1989","unstructured":"Milner, R. Communication and Concurrency. Prentice Hall (1989)."},{"key":"e_1_3_1_33_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44585-4_2"},{"key":"e_1_3_1_34_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-67067-2_7"},{"key":"e_1_3_1_35_2","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539793254571"},{"key":"e_1_3_1_36_2","doi-asserted-by":"publisher","DOI":"10.1145\/263699.263712"},{"key":"e_1_3_1_37_2","doi-asserted-by":"publisher","DOI":"10.1145\/349299.349314"},{"key":"e_1_3_1_38_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45294-X_25"},{"key":"e_1_3_1_39_2","doi-asserted-by":"publisher","DOI":"10.1007\/BFB0054170"},{"key":"e_1_3_1_40_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-11494-7_22"},{"volume-title":"Technical Report MIT-LCS-TR-776","author":"Rinard M.","key":"e_1_3_1_41_2","unstructured":"Rinard, M. Credible Compilation. Technical Report MIT-LCS-TR-776. MIT (199)."},{"key":"e_1_3_1_42_2","volume-title":"Ph.D. Dissertation","author":"Samet H.","year":"1975","unstructured":"Samet, H. Automatically proving the correctness of translations involvingoptimized code \u2014Research sponsored by Advanced Research Projects Agency, ARPA order no. 2494. Ph.D. Dissertation. Stanford University (1975)."},{"key":"e_1_3_1_43_2","doi-asserted-by":"publisher","DOI":"10.1109\/FSCS.1990.89519"},{"key":"e_1_3_1_44_2","doi-asserted-by":"publisher","DOI":"10.1112\/PLMS\/S2-42.1.230"},{"key":"e_1_3_1_45_2","first-page":"67","volume-title":"Report of a Conf. on High Speed Automatic Calculating Machines","author":"Turing A.M.","unstructured":"Turing, A.M. Checking a large routine. In Report of a Conf. on High Speed Automatic Calculating Machines, Univ. Math. Lab., Cambridge, 67\u201369."},{"key":"e_1_3_1_46_2","first-page":"332","volume-title":"Proceedings of the Symp. on Logic in Computer Science","author":"Vardi M.Y.","year":"1986","unstructured":"Vardi, M.Y. and Wolper, P. An automata-theoretic approach to automatic program verification (Preliminary Report). In Proceedings of the Symp. on Logic in Computer Science. IEEE Computer Society (June 1986), 332\u2013344."},{"key":"e_1_3_1_47_2","volume-title":"Planning and Coding of Problems for an Electronic Computing Instrument: Report on the Mathematical and Logical Aspects of an Electronic Computing Instrument","author":"Von Neumann J.","year":"1947","unstructured":"Von Neumann, J. and Goldstine, H.H. Planning and Coding of Problems for an Electronic Computing Instrument: Report on the Mathematical and Logical Aspects of an Electronic Computing Instrument. Institute for Advanced Study (1947\u20131951).)."},{"key":"e_1_3_1_48_2","doi-asserted-by":"publisher","DOI":"10.1145\/268999.269003"},{"key":"e_1_3_1_49_2","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462164"},{"key":"e_1_3_1_50_2","doi-asserted-by":"publisher","DOI":"10.1007\/S10703-005-3402-Z"}],"container-title":["Communications of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3689624","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3689624","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T01:09:47Z","timestamp":1750295387000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3689624"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,1,22]]},"references-count":49,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2025,2]]}},"alternative-id":["10.1145\/3689624"],"URL":"https:\/\/doi.org\/10.1145\/3689624","relation":{},"ISSN":["0001-0782","1557-7317"],"issn-type":[{"type":"print","value":"0001-0782"},{"type":"electronic","value":"1557-7317"}],"subject":[],"published":{"date-parts":[[2025,1,22]]},"assertion":[{"value":"2023-06-16","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-01-22","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}