{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,28]],"date-time":"2026-02-28T07:36:28Z","timestamp":1772264188646,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":40,"publisher":"ACM","license":[{"start":{"date-parts":[[2024,7,10]],"date-time":"2024-07-10T00:00:00Z","timestamp":1720569600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2024,7,10]]},"DOI":"10.1145\/3663529.3663854","type":"proceedings-article","created":{"date-parts":[[2024,7,10]],"date-time":"2024-07-10T19:43:13Z","timestamp":1720640593000},"page":"351-357","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["How We Built Cedar: A Verification-Guided Approach"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4358-2963","authenticated-orcid":false,"given":"Craig","family":"Disselkoen","sequence":"first","affiliation":[{"name":"Amazon Web Services, Arlington, United States"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9105-4922","authenticated-orcid":false,"given":"Aaron","family":"Eline","sequence":"additional","affiliation":[{"name":"Amazon Web Services, Arlington, United States"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9899-6226","authenticated-orcid":false,"given":"Shaobo","family":"He","sequence":"additional","affiliation":[{"name":"Amazon Web Services, Santa Clara, United States"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4880-4150","authenticated-orcid":false,"given":"Kyle","family":"Headley","sequence":"additional","affiliation":[{"name":"Unaffiliated, Arlington, United States"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2759-9223","authenticated-orcid":false,"given":"Michael","family":"Hicks","sequence":"additional","affiliation":[{"name":"Amazon Web Services, Arlington, United States \/ University of Maryland, College Park, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2724-0974","authenticated-orcid":false,"given":"Kesha","family":"Hietala","sequence":"additional","affiliation":[{"name":"Amazon Web Services, Arlington, United States"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1273-5990","authenticated-orcid":false,"given":"John","family":"Kastner","sequence":"additional","affiliation":[{"name":"Amazon Web Services, Arlington, United States"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0007-1184-7206","authenticated-orcid":false,"given":"Anwar","family":"Mamat","sequence":"additional","affiliation":[{"name":"University of Maryland, College Park, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4814-5148","authenticated-orcid":false,"given":"Matt","family":"McCutchen","sequence":"additional","affiliation":[{"name":"Unaffiliated, Arlington, United States"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5143-8940","authenticated-orcid":false,"given":"Neha","family":"Rungta","sequence":"additional","affiliation":[{"name":"Amazon Web Services, Santa Clara, United States"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0000-2698-0260","authenticated-orcid":false,"given":"Bhakti","family":"Shah","sequence":"additional","affiliation":[{"name":"University of Chicago, Chicago, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1155-2711","authenticated-orcid":false,"given":"Emina","family":"Torlak","sequence":"additional","affiliation":[{"name":"Amazon Web Services, Seattle, United States"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7780-2122","authenticated-orcid":false,"given":"Andrew","family":"Wells","sequence":"additional","affiliation":[{"name":"Amazon Web Services, Santa Clara, United States"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,7,10]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"NASA Formal Methods Symposium. 88\u2013108","author":"Astrauskas Vytautas","year":"2022","unstructured":"Vytautas Astrauskas, Aurel B\u00edl\u1ef3, Jon\u00e1\u0161 Fiala, Zachary Grannan, Christoph Matheja, Peter M\u00fcller, Federico Poli, and Alexander J Summers. 2022. The Prusti project: Formal verification for Rust. In NASA Formal Methods Symposium. 88\u2013108."},{"key":"e_1_3_2_1_2_1","unstructured":"Clark Barrett Pascal Fontaine and Cesare Tinelli. 2016. The Satisfiability Modulo Theories Library (SMT-LIB). www.SMT-LIB.org."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3605157.3605170"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3510003.3510230"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3477132.3483540"},{"key":"e_1_3_2_1_6_1","unstructured":"2024. cargo-fuzz. https:\/\/github.com\/rust-fuzz\/cargo-fuzz"},{"key":"e_1_3_2_1_7_1","unstructured":"2024. Cedar Language. https:\/\/www.cedarpolicy.com\/en"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/351240.351266"},{"key":"e_1_3_2_1_9_1","unstructured":"David R. Cok Gary T. Leavens and Mattias Ulbrich. 2022. Java Modeling Language (JML) Reference Manual. https:\/\/www.openjml.org\/"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","unstructured":"The Coq Development Team. 2024. The Coq Proof Assistant. Zenodo. https:\/\/doi.org\/10.5281\/zenodo.5846982 10.5281\/zenodo.5846982","DOI":"10.5281\/zenodo.5846982"},{"key":"e_1_3_2_1_11_1","volume-title":"Proc. ACM Program. Lang., 8, OOPSLA1","author":"Cutler Joseph W.","year":"2024","unstructured":"Joseph W. Cutler, Craig Disselkoen, Aaron Eline, Shaobo He, Kyle Headley, Michael Hicks, Kesha Hietala, Eleftherios Ioannidis, John Kastner, Anwar Mamat, Darin McAdams, Matt McCutchen, Neha Rungta, Emina Torlak, and Andrew M. Wells. 2024. Cedar: A New Language for Expressive, Fast, Safe, and Analyzable Authorization. Proc. ACM Program. Lang., 8, OOPSLA1 (2024)."},{"key":"e_1_3_2_1_12_1","volume-title":"International Conference on Formal Engineering Methods. 90\u2013105","author":"Denis Xavier","year":"2022","unstructured":"Xavier Denis, Jacques-Henri Jourdan, and Claude March\u00e9. 2022. Creusot: a foundry for the deductive verification of Rust programs. In International Conference on Formal Engineering Methods. 90\u2013105."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"crossref","unstructured":"Craig Disselkoen Aaron Eline Shaobo He Kyle Headley Michael Hicks Kesha Hietala John Kastner Anwar Mamat Matt McCutchen Neha Rungta Bhakti Shah Emina Torlak and Andrew Wells. 2024. How We Built Cedar: A Verification-Guided Approach. arxiv:2407.01688. arxiv:2407.01688","DOI":"10.1145\/3663529.3663854"},{"key":"e_1_3_2_1_14_1","volume-title":"1st Summit on Advances in Programming Languages (SNAPL","author":"Ernst Michael D","year":"2015","unstructured":"Michael D Ernst, Dan Grossman, Jon Jacky, Calvin Loncaric, Stuart Pernsteiner, Zachary Tatlock, Emina Torlak, and Xi Wang. 2015. Toward a dependability case language and workflow for a radiation therapy system. In 1st Summit on Advances in Programming Languages (SNAPL 2015)."},{"key":"e_1_3_2_1_15_1","volume-title":"Role-Based Access Control. In 15th National Computer Security Conference.","author":"Ferraiolo David F.","unstructured":"David F. Ferraiolo and D. Richard Kuhn. 1992. Role-Based Access Control. In 15th National Computer Security Conference."},{"key":"e_1_3_2_1_16_1","volume-title":"Computer Aided Verification","author":"Filli\u00e2tre Jean-Christophe","unstructured":"Jean-Christophe Filli\u00e2tre and Claude March\u00e9. 2007. The Why\/Krakatoa\/Caduceus Platform for Deductive Program Verification. In Computer Aided Verification. Springer Verlag, Berlin, Heidelberg. 173\u2013177. https:\/\/www.lri.fr\/~filliatr\/ftp\/publis\/cav07.pdf"},{"key":"e_1_3_2_1_17_1","unstructured":"The F^\u22c6 Development Team. 2024. F^\u22c6 : A proof-oriented programming language. https:\/\/www.fstar-lang.org"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2007.68"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3378426"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3547647"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2015.33"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICST.2016.37"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1498765.1498787"},{"key":"e_1_3_2_1_24_1","unstructured":"2024. The Kani Rust Verifier. https:\/\/model-checking.github.io\/kani\/"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","unstructured":"Richard Kuhn Raghu N. Kacker and Yu Lei. 2012. Combinatorial Coverage Measurement:. https:\/\/doi.org\/10.6028\/NIST.IR.7878 10.6028\/NIST.IR.7878","DOI":"10.6028\/NIST.IR.7878"},{"key":"e_1_3_2_1_26_1","volume-title":"Proc. ACM Program. Lang., 7, OOPSLA1","author":"Lattuada Andrea","year":"2023","unstructured":"Andrea Lattuada, Travis Hance, Chanhee Cho, Matthias Brun, Isitha Subasinghe, Yi Zhou, Jon Howell, Bryan Parno, and Chris Hawblitzel. 2023. Verus: Verifying Rust Programs using Linear Ghost Types. Proc. ACM Program. Lang., 7, OOPSLA1 (2023), Article 85, apr."},{"key":"e_1_3_2_1_27_1","volume-title":"ERTS 2016: Embedded Real Time Software and Systems, 8th European Congress.","author":"Leroy Xavier","year":"2016","unstructured":"Xavier Leroy, Sandrine Blazy, Daniel K\u00e4stner, Bernhard Schommer, Markus Pister, and Christian Ferdinand. 2016. CompCert-a formally verified optimizing compiler. In ERTS 2016: Embedded Real Time Software and Systems, 8th European Congress."},{"key":"e_1_3_2_1_28_1","unstructured":"2024. libFuzzer - a library for coverage-guided fuzz testing. https:\/\/llvm.org\/docs\/LibFuzzer.html"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.21105\/joss.01891"},{"key":"e_1_3_2_1_30_1","first-page":"100","article-title":"Differential testing for software","volume":"10","author":"McKeeman William M","year":"1998","unstructured":"William M McKeeman. 1998. Differential testing for software. Digital Technical Journal, 10, 1 (1998), 100\u2013107.","journal-title":"Digital Technical Journal"},{"key":"e_1_3_2_1_31_1","unstructured":"MISRA Ltd. 2023. MISRA-C:2004 Guidelines for the use of the C language in Critical Systems. Motor Industry Software Reliability Association. www.misra.org.uk"},{"key":"e_1_3_2_1_32_1","volume-title":"Proceedings 28","author":"de Moura Leonardo","year":"2021","unstructured":"Leonardo de Moura and Sebastian Ullrich. 2021. The Lean 4 theorem prover and programming language. In Automated Deduction\u2013CADE 28: 28th International Conference on Automated Deduction, Virtual Event, July 12\u201315, 2021, Proceedings 28. 625\u2013635."},{"key":"e_1_3_2_1_33_1","volume-title":"Paulson","author":"Nipkow Tobias","year":"2021","unstructured":"Tobias Nipkow, Markus Wenzel, and Lawrence C. Paulson. 2021. Isabelle\/HOL: a proof assistant for higher-order logic. Springer-Verlag, Berlin, Heidelberg. https:\/\/isabelle.in.tum.de\/doc\/tutorial.pdf"},{"key":"e_1_3_2_1_34_1","volume-title":"Proceedings of the 6th International Workshop on Automation of Software Test.","author":"Micha\u0142 H.","year":"2011","unstructured":"Micha\u0142 H. Pa\u0142 ka, Koen Claessen, Alejandro Russo, and John Hughes. 2011. Testing an optimising compiler by generating random lambda terms. In Proceedings of the 6th International Workshop on Automation of Software Test."},{"key":"e_1_3_2_1_35_1","volume-title":"2020 IEEE Symposium on Security and Privacy (SP). 983\u20131002","author":"Protzenko Jonathan","year":"2020","unstructured":"Jonathan Protzenko, Bryan Parno, Aymeric Fromherz, Chris Hawblitzel, Marina Polubelova, Karthikeyan Bhargavan, Benjamin Beurdouche, Joonwon Choi, Antoine Delignat-Lavaud, and C\u00e9dric Fournet. 2020. Evercrypt: A fast, verified, cross-platform cryptographic provider. In 2020 IEEE Symposium on Security and Privacy (SP). 983\u20131002."},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110261"},{"key":"e_1_3_2_1_37_1","unstructured":"Alastair Reid Luke Church Shaked Flur Sarah de Haas Maritza Johnson and Ben Laurie. 2020. Towards making formal methods normal: meeting developers where they are. arXiv preprint arXiv:2010.16345."},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815411"},{"key":"e_1_3_2_1_39_1","unstructured":"2024. The TinyTodo Example. https:\/\/github.com\/cedar-policy\/cedar-examples\/tree\/release\/3.0.x\/tinytodo"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993532"}],"event":{"name":"FSE '24: 32nd ACM International Conference on the Foundations of Software Engineering","location":"Porto de Galinhas Brazil","acronym":"FSE '24","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering"]},"container-title":["Companion Proceedings of the 32nd ACM International Conference on the Foundations of Software Engineering"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3663529.3663854","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3663529.3663854","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T23:44:22Z","timestamp":1750290262000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3663529.3663854"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,7,10]]},"references-count":40,"alternative-id":["10.1145\/3663529.3663854","10.1145\/3663529"],"URL":"https:\/\/doi.org\/10.1145\/3663529.3663854","relation":{},"subject":[],"published":{"date-parts":[[2024,7,10]]},"assertion":[{"value":"2024-07-10","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}