{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,1]],"date-time":"2026-05-01T16:44:45Z","timestamp":1777653885040,"version":"3.51.4"},"reference-count":59,"publisher":"Association for Computing Machinery (ACM)","issue":"10","license":[{"start":{"date-parts":[[2021,9,22]],"date-time":"2021-09-22T00:00:00Z","timestamp":1632268800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000879","name":"Sloan Foundation","doi-asserted-by":"crossref","award":["G-2020-13917"],"award-info":[{"award-number":["G-2020-13917"]}],"id":[{"id":"10.13039\/100000879","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CNS 1801426"],"award-info":[{"award-number":["CNS 1801426"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Commun. ACM"],"published-print":{"date-parts":[[2021,10]]},"abstract":"<jats:p>The pursuit of responsible AI raises the ante on both the trustworthy computing and formal methods communities.<\/jats:p>","DOI":"10.1145\/3448248","type":"journal-article","created":{"date-parts":[[2021,9,22]],"date-time":"2021-09-22T14:37:02Z","timestamp":1632321422000},"page":"64-71","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":136,"title":["Trustworthy AI"],"prefix":"10.1145","volume":"64","author":[{"given":"Jeannette M.","family":"Wing","sequence":"first","affiliation":[{"name":"Columbia University, New York, NY"}]}],"member":"320","published-online":{"date-parts":[[2021,9,22]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Trustworthy AI Symposium","author":"Agrawal S.","year":"2019","unstructured":"Agrawal , S. and Wing , J.M . Trustworthy AI Symposium . Columbia University, (Oct. 30- Nov. 1, 2019 ); https:\/\/datascience.columbia.edu\/trustworthy-ai-symposium. Agrawal, S. and Wing, J.M. Trustworthy AI Symposium. Columbia University, (Oct. 30-Nov. 1, 2019); https:\/\/datascience.columbia.edu\/trustworthy-ai-symposium."},{"key":"e_1_2_1_2_1","volume-title":"Proceedings of ACM OOPSLA '17","author":"Albarghouthi A.","unstructured":"Albarghouthi , A. , D'Antoni , L. , Drews , S. and Nori , A . FairSquare: Probabilistic verification of program fairness . In Proceedings of ACM OOPSLA '17 . Albarghouthi, A., D'Antoni, L., Drews, S. and Nori, A. FairSquare: Probabilistic verification of program fairness. In Proceedings of ACM OOPSLA '17."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.489079"},{"key":"e_1_2_1_4_1","volume-title":"ProPublica (May 23","author":"Angwin J.","year":"2016","unstructured":"Angwin , J. , Larson , J. , Mattu , S. and Kirchner , L . Machine bias . ProPublica (May 23 , 2016 ). Angwin, J., Larson, J., Mattu, S. and Kirchner, L. Machine bias. ProPublica (May 23, 2016)."},{"key":"e_1_2_1_6_1","volume-title":"Formal Methods in Computer-Aided Design","author":"Baumgartner J.","year":"2006","unstructured":"Baumgartner , J. Integrating formal verification into mainstream verification: The IBM experience . Formal Methods in Computer-Aided Design , Haifa, Israel , 2006 . Baumgartner, J. Integrating formal verification into mainstream verification: The IBM experience. Formal Methods in Computer-Aided Design, Haifa, Israel, 2006."},{"key":"e_1_2_1_7_1","volume-title":"Proceedings of the 2nd Summit on Advances in Programming Languages","author":"Bhargavan K.","year":"2017","unstructured":"Bhargavan , K. et al. Everest: Towards a verified, drop-in replacement of HTTPS . In Proceedings of the 2nd Summit on Advances in Programming Languages , May 2017 . Bhargavan, K. et al. Everest: Towards a verified, drop-in replacement of HTTPS. In Proceedings of the 2nd Summit on Advances in Programming Languages, May 2017."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.18637\/jss.v076.i01"},{"key":"e_1_2_1_9_1","unstructured":"Center for Trustworthy Machine Learning; https:\/\/ctml.psu.edu  Center for Trustworthy Machine Learning; https:\/\/ctml.psu.edu"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3132747.3132776"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815402"},{"key":"e_1_2_1_12_1","volume-title":"Proceedings of FATML","author":"Chouldechova A.","year":"2016","unstructured":"Chouldechova , A. Fair prediction with disparate impact: A study of bias in recidivism prediction instruments . In Proceedings of FATML , 2016 . Chouldechova, A. Fair prediction with disparate impact: A study of bias in recidivism prediction instruments. In Proceedings of FATML, 2016."},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-10003-2_69"},{"key":"e_1_2_1_14_1","volume-title":"Counterexample-guided abstraction refinement","author":"Clarke E.","year":"1855","unstructured":"Clarke , E. , Grumberg , O. , Jha , S. , Lu , Y. and Veith , H . Counterexample-guided abstraction refinement . Computer Aided Verification. E.A. Emerson, A.P. Sistla, eds. Lecture Notes in Computer Science 1855 (2000). Springer , Berlin, Heidelberg. Clarke, E., Grumberg, O., Jha, S., Lu, Y. and Veith, H. Counterexample-guided abstraction refinement. Computer Aided Verification. E.A. Emerson, A.P. Sistla, eds. Lecture Notes in Computer Science 1855 (2000). Springer, Berlin, Heidelberg."},{"key":"e_1_2_1_15_1","volume-title":"Formal reasoning about the security of Amazon Web Services,\" Proceedings of the International Conference on Computer Aided Verification","author":"Cook B.","year":"2018","unstructured":"Cook , B. Formal reasoning about the security of Amazon Web Services,\" Proceedings of the International Conference on Computer Aided Verification , Volume 10981 , 2018 . Cook, B. Formal reasoning about the security of Amazon Web Services,\" Proceedings of the International Conference on Computer Aided Verification, Volume 10981, 2018."},{"key":"e_1_2_1_16_1","volume-title":"Defense Advanced Research Projects Agency","author":"Explainable","year":"2016","unstructured":"DARPA. Explainable AI (XAI) Program. Matt Turek , Defense Advanced Research Projects Agency , 2016 ; https:\/\/www.darpa.mil\/program\/explainable-artificial-intelligence. DARPA. Explainable AI (XAI) Program. Matt Turek, Defense Advanced Research Projects Agency, 2016; https:\/\/www.darpa.mil\/program\/explainable-artificial-intelligence."},{"key":"e_1_2_1_17_1","volume-title":"Amazon scraps secret AI recruiting tool that showed bias against women","author":"Dastin J.","year":"2018","unstructured":"Dastin , J. Amazon scraps secret AI recruiting tool that showed bias against women . Reuters , Oct. 9, 2018 . Dastin, J. Amazon scraps secret AI recruiting tool that showed bias against women. Reuters, Oct. 9, 2018."},{"key":"e_1_2_1_18_1","volume-title":"Proceedings of the AAAI Spring Symp. Workshop on Verification of Neural Networks","author":"Dreossi T.","year":"2019","unstructured":"Dreossi , T. , Ghosh , S. , Sangiovanni-Vincentelli , A.L. and Seshia , S.A . A formalization of robustness for deep neural networks . In Proceedings of the AAAI Spring Symp. Workshop on Verification of Neural Networks , Mar. 2019 . Dreossi, T., Ghosh, S., Sangiovanni-Vincentelli, A.L. and Seshia, S.A. A formalization of robustness for deep neural networks. In Proceedings of the AAAI Spring Symp. Workshop on Verification of Neural Networks, Mar. 2019."},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25540-4_25"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2090236.2090255"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/11681878"},{"key":"e_1_2_1_22_1","volume-title":"Proceedings of CVPR","author":"Eykholt K.","year":"2017","unstructured":"Eykholt , K. et al. Robust physical-world attacks on deep learning visual classification . In Proceedings of CVPR 2017 . Eykholt, K. et al. Robust physical-world attacks on deep learning visual classification. In Proceedings of CVPR 2017."},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1126\/science.aaw4399"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3302509.3311053"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.5555\/2789272.2886795"},{"key":"e_1_2_1_26_1","volume-title":"Trustworthy computing. Microsoft memo (Jan. 15","author":"Gates B.","year":"2002","unstructured":"Gates , B. Trustworthy computing. Microsoft memo (Jan. 15 , 2002 ); wired.com Gates, B. Trustworthy computing. Microsoft memo (Jan. 15, 2002); wired.com"},{"key":"e_1_2_1_27_1","volume-title":"Proceedings of 12th USENIX Symp. Operating Systems Design and Implementation","author":"Gu R.","year":"2016","unstructured":"Gu , R. , Shao , Z. , Chen , H. , Wu , X.N. , Kim , J. , Sjberg , V. and Costanzo , D . Certikos: An extensible architecture for building certified concurrent OS kernels . Proceedings of 12th USENIX Symp. Operating Systems Design and Implementation , 2016 . Gu, R., Shao, Z., Chen, H., Wu, X.N., Kim, J., Sjberg, V. and Costanzo, D. Certikos: An extensible architecture for building certified concurrent OS kernels. Proceedings of 12th USENIX Symp. Operating Systems Design and Implementation, 2016."},{"key":"e_1_2_1_28_1","volume-title":"Program Synthesis. Foundations and Trends\u00ae in Programming Languages","author":"Gulwani S.","year":"2017","unstructured":"Gulwani , S. , Polozov , O. and Singh , R . Program Synthesis. Foundations and Trends\u00ae in Programming Languages . Now Publishers Inc ., 2017 . Gulwani, S., Polozov, O. and Singh, R. Program Synthesis. Foundations and Trends\u00ae in Programming Languages. Now Publishers Inc., 2017."},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2003.1210044"},{"key":"e_1_2_1_30_1","volume-title":"Proceedings of the 11th USENIX Symp. Operating Systems Design and Implementation","author":"Hawblitzel C.","year":"2014","unstructured":"Hawblitzel , C. , Howell , J. , Lorch , J.R. , Narayan , A. , Parno , B. , Zhang , D. and Zill , B . Ironclad apps: End-to-end security via automated full-system verification . In Proceedings of the 11th USENIX Symp. Operating Systems Design and Implementation , 2014 . Hawblitzel, C., Howell, J., Lorch, J.R., Narayan, A., Parno, B., Zhang, D. and Zill, B. Ironclad apps: End-to-end security via automated full-system verification. In Proceedings of the 11th USENIX Symp. Operating Systems Design and Implementation, 2014."},{"key":"e_1_2_1_31_1","volume-title":"Fairness indicators: Thinking about fairness evaluation","author":"Hutchinson B.","year":"2020","unstructured":"Hutchinson , B. , Mitchell , M. , Xu , C. , Doshi , T. Fairness indicators: Thinking about fairness evaluation , 2020 ; https:\/\/www.tensorflow.org\/tfx\/fairness_indicators\/guidance. Hutchinson, B., Mitchell, M., Xu, C., Doshi, T. Fairness indicators: Thinking about fairness evaluation, 2020; https:\/\/www.tensorflow.org\/tfx\/fairness_indicators\/guidance."},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3365365.3382216"},{"key":"e_1_2_1_33_1","volume-title":"Proceedings of Innovations in Theoretical Computer Science","author":"Kleinberg J.","year":"2017","unstructured":"Kleinberg , J. , Mullainathan , S. Raghavan , M. Inherent trade-offs in the fair determination of risk scores . In Proceedings of Innovations in Theoretical Computer Science , 2017 . Kleinberg, J., Mullainathan, S. Raghavan, M. Inherent trade-offs in the fair determination of risk scores. In Proceedings of Innovations in Theoretical Computer Science, 2017."},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3293880.3294106"},{"key":"e_1_2_1_35_1","volume-title":"Proceedings of the PAPM\/PROBMIV'01 Tools Session.","author":"Kwiatkowska M.","year":"2001","unstructured":"Kwiatkowska , M. , Norman , G. and Parker , D . PRISM: Probabilistic Symbolic Model Checker . In Proceedings of the PAPM\/PROBMIV'01 Tools Session. Sept. 2001 , 7--12. Available as Technical Report 760\/ 2001, University of Dortmund. Kwiatkowska, M., Norman, G. and Parker, D. PRISM: Probabilistic Symbolic Model Checker. In Proceedings of the PAPM\/PROBMIV'01 Tools Session. Sept. 2001, 7--12. Available as Technical Report 760\/2001, University of Dortmund."},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1977.229904"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.5555\/3495724.3497273"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.21236\/ADA116035"},{"key":"e_1_2_1_39_1","volume-title":"Fairness in machine learning models","author":"Microsoft Azure","year":"2020","unstructured":"Microsoft Azure blog. Fairness in machine learning models , 2020 ; https:\/\/docs.microsoft.com\/en-us\/azure\/machine-learning\/concept-fairness-ml Microsoft Azure blog. Fairness in machine learning models, 2020; https:\/\/docs.microsoft.com\/en-us\/azure\/machine-learning\/concept-fairness-ml"},{"key":"e_1_2_1_40_1","volume-title":"Proceedings of FAT*","author":"Narayanan A.","year":"2018","unstructured":"Narayanan , A. 21 Definitions of fairness and their politics . In Proceedings of FAT* 2018 . Tutorial; https:\/\/www.youtube.com\/watch?v=jIXIuYdnyyk. Narayanan, A. 21 Definitions of fairness and their politics. In Proceedings of FAT* 2018. Tutorial; https:\/\/www.youtube.com\/watch?v=jIXIuYdnyyk."},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.17226\/6161"},{"key":"e_1_2_1_42_1","volume-title":"National AI Institutes Call for Proposals","author":"National Science Foundation.","year":"2019","unstructured":"National Science Foundation. National AI Institutes Call for Proposals , 2019 ; https:\/\/www.nsf.gov\/pubs\/2020\/nsf20503\/nsf20503.htm. National Science Foundation. National AI Institutes Call for Proposals, 2019; https:\/\/www.nsf.gov\/pubs\/2020\/nsf20503\/nsf20503.htm."},{"key":"e_1_2_1_43_1","volume-title":"NSF Program on Fairness in Artificial Intelligence in Collaboration with Amazon (FAI)","author":"National Science Foundation.","year":"2020","unstructured":"National Science Foundation. NSF Program on Fairness in Artificial Intelligence in Collaboration with Amazon (FAI) , 2020 ; https:\/\/www.nsf.gov\/funding\/pgm_summ.jsp?pims_id=505651 National Science Foundation. NSF Program on Fairness in Artificial Intelligence in Collaboration with Amazon (FAI), 2020; https:\/\/www.nsf.gov\/funding\/pgm_summ.jsp?pims_id=505651"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/2699417"},{"key":"e_1_2_1_45_1","unstructured":"Networking and Information Technology Research and Development Subcommittee Machine Learning and Artificial Intelligence Subcommittee and the Special Cyber Operations Research and Engineering Subcommittee of the National Science and Technology Council. Artificial Intelligence and Cybersecurity: Opportunities and Challenges. Public Report; https:\/\/www.nitrd.gov\/pubs\/AI-CS-Tech-Summary-2020.pdf.  Networking and Information Technology Research and Development Subcommittee Machine Learning and Artificial Intelligence Subcommittee and the Special Cyber Operations Research and Engineering Subcommittee of the National Science and Technology Council. Artificial Intelligence and Cybersecurity: Opportunities and Challenges. Public Report; https:\/\/www.nitrd.gov\/pubs\/AI-CS-Tech-Summary-2020.pdf."},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.5555\/3281334"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/248621.248624"},{"key":"e_1_2_1_49_1","volume-title":"Proceedings of 22nd Intern. Conf. Functional Programming","author":"Protzenko J.","year":"2017","unstructured":"Protzenko , J. et al. Verified low-level programming embedded in F* . In Proceedings of 22nd Intern. Conf. Functional Programming , May 2017 . Protzenko, J. et al. Verified low-level programming embedded in F*. In Proceedings of 22nd Intern. Conf. Functional Programming, May 2017."},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-11494-7_22"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-01090-4_2"},{"key":"e_1_2_1_52_1","volume-title":"CNET","author":"Shankland S.","unstructured":"Shankland , S. Facebook starts building AI with an ethical compass . CNET , 2018; https:\/\/www.cnet.com\/news\/facebook-starts-building-ai-with-an-ethical-compass\/. Shankland, S. Facebook starts building AI with an ethical compass. CNET, 2018; https:\/\/www.cnet.com\/news\/facebook-starts-building-ai-with-an-ethical-compass\/."},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1126\/science.aag3311"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.3174\/ajnr.A4931"},{"key":"e_1_2_1_55_1","volume-title":"IBM","author":"Varshney K.","unstructured":"Varshney , K. Introducing AI Fairness 360 . IBM , 2018; https:\/\/www.ibm.com\/blogs\/research\/2018\/09\/ai-fairness-360\/. Varshney, K. Introducing AI Fairness 360. IBM, 2018; https:\/\/www.ibm.com\/blogs\/research\/2018\/09\/ai-fairness-360\/."},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.5555\/3277203.3277323"},{"key":"e_1_2_1_57_1","volume-title":"Proceedings of Neural Information Processing Systems","author":"Wang S.","year":"2018","unstructured":"Wang , S. , Pei , K. , Whitehouse , J. , Yang , J. and Jana , S . Efficient formal safety analysis of neural networks . In Proceedings of Neural Information Processing Systems , 2018 . Wang, S., Pei, K., Whitehouse, J., Yang, J. and Jana, S. Efficient formal safety analysis of neural networks. In Proceedings of Neural Information Processing Systems, 2018."},{"key":"e_1_2_1_58_1","volume-title":"Dec. 3","author":"White House","year":"2020","unstructured":"White House . Executive Order on Promoting the Use of Trustworthy Artificial Intelligence in the Federal Government , Dec. 3 , 2020 ; https:\/\/www.whitehouse.gov\/presidential-actions\/executive-order-promoting-use-trustworthy-artificial-intelligence-federal-government\/. White House. Executive Order on Promoting the Use of Trustworthy Artificial Intelligence in the Federal Government, Dec. 3, 2020; https:\/\/www.whitehouse.gov\/presidential-actions\/executive-order-promoting-use-trustworthy-artificial-intelligence-federal-government\/."},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.5555\/647771.760735"},{"key":"e_1_2_1_60_1","first-page":"901","article-title":"Light DP: Towards automating differential privacy proofs. In Proceedings of the 44th ACM SIGPLAN Symp","volume":"888","author":"Zheng D.","year":"2017","unstructured":"Zheng , D. and Kifer , D . Light DP: Towards automating differential privacy proofs. In Proceedings of the 44th ACM SIGPLAN Symp . Principles of Programming Languages , 2017 , 888 -- 901 . Zheng, D. and Kifer, D. Light DP: Towards automating differential privacy proofs. In Proceedings of the 44th ACM SIGPLAN Symp. Principles of Programming Languages, 2017, 888--901.","journal-title":"Principles of Programming Languages"}],"container-title":["Communications of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3448248","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3448248","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3448248","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:47:41Z","timestamp":1750193261000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3448248"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,9,22]]},"references-count":59,"journal-issue":{"issue":"10","published-print":{"date-parts":[[2021,10]]}},"alternative-id":["10.1145\/3448248"],"URL":"https:\/\/doi.org\/10.1145\/3448248","relation":{},"ISSN":["0001-0782","1557-7317"],"issn-type":[{"value":"0001-0782","type":"print"},{"value":"1557-7317","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,9,22]]},"assertion":[{"value":"2021-09-22","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}