|
| [59] | Secure Distributed Programming with Value-Dependent Types (Swamy, Nikhil, Chen, Juan, Fournet, Cédric, Strub, Pierre-Yves, Bhargavan, Karthikeyan and Yang, Jean), In Proceedings of the 16th ACM SIGPLAN International Conference on Functional Programming, Association for Computing Machinery, 2011. |
|
| [58] | Self-Certification: Bootstrapping Certified Typecheckers in F* with Coq (Strub, Pierre-Yves, Swamy, Nikhil, Fournet, Cedric and Chen, Juan), In Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Association for Computing Machinery, 2012. |
| [57] | Self-Certification: Bootstrapping Certified Typecheckers in F* with Coq (Strub, Pierre-Yves, Swamy, Nikhil, Fournet, Cedric and Chen, Juan), In SIGPLAN Not., Association for Computing Machinery, volume 47, 2012. |
|
| [56] | Fully Abstract Compilation to JavaScript (Fournet, Cedric, Swamy, Nikhil, Chen, Juan, Dagand, Pierre-Evariste, Strub, Pierre-Yves and Livshits, Benjamin), In Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Association for Computing Machinery, 2013. |
| [55] | Verifying Higher-order Programs with the Dijkstra Monad (Nikhil Swamy, Joel Weinberger, Cole Schlesinger, Juan Chen and Benjamin Livshits), In Proceedings of the 34th annual ACM SIGPLAN conference on Programming Language Design and Implementation, 2013. |
| [54] | Fully Abstract Compilation to JavaScript (Fournet, Cedric, Swamy, Nikhil, Chen, Juan, Dagand, Pierre-Evariste, Strub, Pierre-Yves and Livshits, Benjamin), In SIGPLAN Not., Association for Computing Machinery, volume 48, 2013. |
|
| [53] | Probabilistic Relational Verification for Cryptographic Implementations (Barthe, Gilles, Fournet, Cédric, Grégoire, Benjamin, Strub, Pierre-Yves, Swamy, Nikhil and Zanella-Béguelin, Santiago), In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Association for Computing Machinery, 2014. |
| [52] | Gradual Typing Embedded Securely in JavaScript (Swamy, Nikhil, Fournet, Cedric, Rastogi, Aseem, Bhargavan, Karthikeyan, Chen, Juan, Strub, Pierre-Yves and Bierman, Gavin), In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Association for Computing Machinery, 2014. |
| [51] | Gradual Typing Embedded Securely in JavaScript (Swamy, Nikhil, Fournet, Cedric, Rastogi, Aseem, Bhargavan, Karthikeyan, Chen, Juan, Strub, Pierre-Yves and Bierman, Gavin), In SIGPLAN Not., Association for Computing Machinery, volume 49, 2014. |
| [50] | Probabilistic Relational Verification for Cryptographic Implementations (Barthe, Gilles, Fournet, Cédric, Grégoire, Benjamin, Strub, Pierre-Yves, Swamy, Nikhil and Zanella-Béguelin, Santiago), In SIGPLAN Not., Association for Computing Machinery, volume 49, 2014. |
|
| [49] | Dependent Types and Multi-Monadic Effects in F* (Nikhil Swamy, Catalin Hritcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, Cédric Fournet, Pierre-Yves Strub, Markulf Kohlweiss and Jean-Karim Zinzindohoué), In 43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), ACM, 2016. |
| [48] | Towards a Provably Correct Encoding from F* to SMT (Alejandro Aguirre), Inria Internship Report, 2016. |
|
| [47] | HACL*: A Verified Modern Cryptographic Library (Jean-Karim Zinzindohoué, Karthikeyan Bhargavan, Jonathan Protzenko and Benjamin Beurdouche), In ACM Conference on Computer and Communications Security, ACM, 2017. |
| [46] | Implementing and Proving the TLS 1.3 Record Layer (Karthikeyan Bhargavan, Antoine Delignat-Lavaud and Cédric Fournet, Markulf Kohlweiss, Jianyang Pan, Jonathan Protzenko, Aseem Rastogi, Nikhil Swamy, Santiago Zanella Béguelin and Jean Karim Zinzindohoue), In IEEE Security & Privacy, 2017. |
| [45] | Verified Compilation of Space-Efficient Reversible Circuits (Amy, Matthew and Roetteler, Martin and Svore, Krysta M.), In Computer Aided Verification (Majumdar, Rupak, Kunčak, Viktor, eds.), Springer International Publishing, 2017. |
| [44] | Dijkstra Monads for Free (Danel Ahman, Catalin Hritcu, Kenji Maillard, Guido Martínez, Gordon Plotkin, Jonathan Protzenko, Aseem Rastogi and Nikhil Swamy), In 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), ACM, 2017. |
| [43] | Everest: Towards a Verified, Drop-in Replacement of HTTPS (Karthikeyan Bhargavan, Barry Bond, Antoine Delignat-Lavaud, Cédric Fournet, Chris Hawblitzel, Catalin Hritcu, Samin Ishtiaq, Markulf Kohlweiss, Rustan Leino, Jay Lorch, Kenji Maillard, Jianyang Pang, Bryan Parno, Jonathan Protzenko, Tahina Ramananandro, Ashay Rane, Aseem Rastogi, Nikhil Swamy, Laure Thompson, Peng Wang, Santiago Zanella-Béguelin and Jean-Karim Zinzindohoué), In 2nd Summit on Advances in Programming Languages, 2017. |
| [42] | Verified Low-Level Programming Embedded in F* (Jonathan Protzenko, Jean-Karim Zinzindohoué, Aseem Rastogi, Tahina Ramananandro, Peng Wang, Santiago Zanella-Béguelin, Antoine Delignat-Lavaud, Catalin Hritcu, Karthikeyan Bhargavan, Cédric Fournet and Nikhil Swamy), In PACMPL, volume 1, 2017. |
|
| [41] | Recalling a Witness: Foundations and Applications of Monotonic State (Danel Ahman, Cédric Fournet, Catalin Hritcu, Kenji Maillard, Aseem Rastogi and Nikhil Swamy), In PACMPL, volume 2, 2018. |
| [40] | A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations (Niklas Grimm, Kenji Maillard, Cédric Fournet, Catalin Hritcu, Matteo Maffei, Jonathan Protzenko, Tahina Ramananandro, Aseem Rastogi and Nikhil Swamy), In The 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2018. |
|
| [39] | Everparse: Verified Secure Zero-Copy Parsers for Authenticated Message Formats (Ramananandro, Tahina, Delignat-Lavaud, Antoine, Fournet, Cédric, Swamy, Nikhil, Chajed, Tej, Kobeissi, Nadim and Protzenko, Jonathan), In Proceedings of the 28th USENIX Conference on Security Symposium, USENIX Association, 2019. |
| [38] | A Verified, Efficient Embedding of a Verifiable Assembly Language (Aymeric Fromherz, Nick Giannarakis, Chris Hawblitzel, Bryan Parno, Aseem Rastogi and Nikhil Swamy), In PACMPL, 2019. |
| [37] | Wys*: A DSL for Verified Secure Multi-party Computations (Aseem Rastogi, Nikhil Swamy and Michael Hicks), In 8th International Conference on Principles of Security and Trust (POST) (Flemming Nielson, David Sands, eds.), Springer, volume 11426, 2019. |
| [36] | Formally Verified Cryptographic Web Applications in WebAssembly (J. Protzenko, B. Beurdouche, D. Merigoux and K. Bhargavan), In 2019 IEEE Symposium on Security and Privacy (SP), 2019. |
| [35] | Meta-F*: Proof Automation with SMT, Tactics, and Metaprograms (Guido Martínez, Danel Ahman, Victor Dumitrescu, Nick Giannarakis, Chris Hawblitzel, Catalin Hritcu, Monal Narasimhamurthy, Zoe Paraskevopoulou, Clément Pit-Claudel, Jonathan Protzenko, Tahina Ramananandro, Aseem Rastogi and Nikhil Swamy), In 28th European Symposium on Programming (ESOP), Springer, 2019. |
| [34] | The Next 700 Relational Program Logics (Kenji Maillard, Catalin Hritcu, Exequiel Rivas and Antoine Van Muylder), arXiv:1907.05244, 2019. |
| [33] | Dijkstra Monads for All (Kenji Maillard, Danel Ahman, Robert Atkey, Guido Martínez, Catalin Hritcu, Exequiel Rivas and Éric Tanter), In 24th ACM SIGPLAN International Conference on Functional Programming (ICFP), 2019. |
|
| [32] | EverCrypt: A Fast, Verified, Cross-Platform Cryptographic Provider (Protzenko, Jonathan, Parno, Bryan, Fromherz, Aymeric, Hawblitzel, Chris, Polubelova, Marina, Bhargavan, Karthikeyan, Beurdouche, Benjamin, Choi, Joonwon, Delignat-Lavaud, Antoine, Fournet, Cédric, Kulatova, Natalia, Ramananandro, Tahina, Rastogi, Aseem, Swamy, Nikhil, Wintersteiger, Christoph M. and Zanella-Beguelin, Santiago), In 2020 IEEE Symposium on Security and Privacy (SP), 2020. |
| [31] | HACLxN: Verified Generic SIMD Crypto (for All Your Favourite Platforms) (Polubelova, Marina, Bhargavan, Karthikeyan, Protzenko, Jonathan, Beurdouche, Benjamin, Fromherz, Aymeric, Kulatova, Natalia and Zanella-Béguelin, Santiago), In Proceedings of the 2020 ACM SIGSAC Conference on Computer and Communications Security, Association for Computing Machinery, 2020. |
| [30] | Verified Transformations and Hoare Logic: Beautiful Proofs for Ugly Assembly Language (Bosamiya, Jay, Gibson, Sydney, Li, Yao, Parno, Bryan and Hawblitzel, Chris), In Proceedings of the Conference on Verified Software: Theories, Tools, and Experiments (VSTTE), 2020. |
| [29] | SteelCore: An Extensible Concurrent Separation Logic for Effectful Dependently Typed Programs (Nikhil Swamy, Aseem Rastogi, Aymeric Fromherz, Denis Merigoux, Danel Ahman and Guido Martínez), In 25th ACM SIGPLAN International Conference on Functional Programming (ICFP), 2020. |
| [28] | Statically Verified Refinements for Multiparty Protocols (Zhou, Fangyi, Ferreira, Francisco, Hu, Raymond, Neykova, Rumyana and Yoshida, Nobuko), In Proc. ACM Program. Lang., Association for Computing Machinery, volume 4, 2020. |
|
| [27] | Verified Functional Programming of an Abstract Interpreter (Franceschino, Lucas and Pichardie, David and Talpin, Jean-Pierre), In Static Analysis (Dr\uagoi, Cezara, Mukherjee, Suvam, Namjoshi, Kedar, eds.), Springer International Publishing, 2021. |
| [26] | A Tutorial-Style Introduction to $}{\$\backslashtextsf \DY\^\backslashstar $}{\$ (Bhargavan, Karthikeyan and Bichhawat, Abhishek and Do, Quoc Huy and Hosseyni, Pedram and Küsters, Ralf and Schmitz, Guido and Würtele, Tim), Chapter in (Dougherty, Daniel, Meseguer, José, Mödersheim, Sebastian Alexander, Rowe, Paul, eds.), Springer International Publishing, 2021. |
| [25] | Verification of a Merkle Patricia Tree Library Using F (Sota Sato, Ryotaro Banno, Junji Furuse, Kohei Suenaga and Atsushi Igarashi), In ArXiv, volume abs/2106.04826, 2021. |
| [24] | An In-Depth Symbolic Security Analysis of the ACME Standard (Bhargavan, Karthikeyan, Bichhawat, Abhishek, Do, Quoc Huy, Hosseyni, Pedram, Küsters, Ralf, Schmitz, Guido and Würtele, Tim), In Proceedings of the 2021 ACM SIGSAC Conference on Computer and Communications Security, Association for Computing Machinery, 2021. |
| [23] | $\text{DY}^{\star}$: A Modular Symbolic Verification Framework for Executable Cryptographic Protocol Code (Bhargavan, Karthikeyan, Bichhawat, Abhishek, Do, Quoc Huy, Hosseyni, Pedram, Küsters, Ralf, Schmitz, Guido and Würtele, Tim), In 2021 IEEE European Symposium on Security and Privacy (EuroS&P), volume , 2021. |
| [22] | A Security Model and Fully Verified Implementation for the IETF QUIC Record Layer (Delignat-Lavaud, Antoine, Fournet, Cédric, Parno, Bryan, Protzenko, Jonathan, Ramananandro, Tahina, Bosamiya, Jay, Lallemand, Joseph, Rakotonirina, Itsaka and Zhou, Yi), In 2021 IEEE Symposium on Security and Privacy (SP), volume , 2021. |
| [21] | FastVer: Making Data Integrity a Commodity (Arasu, Arvind, Chandramouli, Badrish, Gehrke, Johannes, Ghosh, Esha, Kossmann, Donald, Protzenko, Jonathan, Ramamurthy, Ravi, Ramananandro, Tahina, Rastogi, Aseem, Setty, Srinath, Swamy, Nikhil, van Renen, Alexander and Xu, Min), In Proceedings of the 2021 International Conference on Management of Data, Association for Computing Machinery, 2021. |
| [20] | Programming and Proving with Indexed Effects (Aseem Rastogi, Guido Martínez, Aymeric Fromherz, Tahina Ramananandro and Nikhil Swamy), 2021. |
| [19] | Steel: Proof-oriented Programming in a Dependently Typed Concurrent Separation Logic (Aymeric Fromherz, Aseem Rastogi, Nikhil Swamy, Sydney Gibson, Guido Martínez, Denis Merigoux and Tahina Ramananandro), In 25th ACM SIGPLAN International Conference on Functional Programming (ICFP), 2021. |
| [18] | DICE*: A Formally Verified Implementation of DICE Measured Boot (Zhe Tao, Aseem Rastogi, Naman Gupta, Kapil Vaswani and Aditya V. Thakur), In 30th Usenix Security Symposium, 2021. |
| [17] | Catala: A Programming Language for the Law (Merigoux, Denis, Chataing, Nicolas and Protzenko, Jonathan), In Proc. ACM Program. Lang., Association for Computing Machinery, volume 5, 2021. |
|
| [16] | Certified Mergeable Replicated Data Types (Soundarapandian, Vimala, Kamath, Adharsh, Nagar, Kartik and Sivaramakrishnan, KC), In Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, Association for Computing Machinery, 2022. |
| [15] | Noise*: A Library of Verified High-Performance Secure Channel Protocol Implementations (Ho, Son, Protzenko, Jonathan, Bichhawat, Abhishek and Bhargavan, Karthikeyan), In 2022 IEEE Symposium on Security and Privacy (SP), 2022. |
| [14] | Hardening Attack Surfaces with Formally Proven Binary Format Parsers (Nikhil Swamy, Tahina Ramananandro, Aseem Rastogi, Irina Spiridonova, Haobin Ni, Dmitry Malloy, Juan Vazquez, Michael Tang, Omar Cardona and Arti Gupta), In Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI '22), June 13–17, 2022, San Diego, CA, USA, 2022. |
| [13] | Aeneas: Rust Verification by Functional Translation (Ho, Son and Protzenko, Jonathan), In Proc. ACM Program. Lang., Association for Computing Machinery, volume 6, 2022. |
| [12] | Provably-Safe Multilingual Software Sandboxing using WebAssembly (Bosamiya, Jay, Lim, Wen Shih and Parno, Bryan), In Proceedings of the USENIX Security Symposium, 2022. |
|
| [11] | Comparse: Provably Secure Formats for Cryptographic Protocols (Wallez, Théophile, Protzenko, Jonathan and Bhargavan, Karthikeyan), In Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security, Association for Computing Machinery, 2023. |
| [10] | ASN1*: Provably Correct, Non-Malleable Parsing for ASN.1 DER (Ni, Haobin, Delignat-Lavaud, Antoine, Fournet, Cédric, Ramananandro, Tahina and Swamy, Nikhil), In Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, Association for Computing Machinery, 2023. |
| [9] | TreeSync: Authenticated Group Management for Messaging Layer Security (Théophile Wallez, Jonathan Protzenko, Benjamin Beurdouche and Karthikeyan Bhargavan), In Proceedings of the 32th USENIX Conference on Security Symposium, USENIX Association, 2023. |
| [8] | FastVer2: A Provably Correct Monitor for Concurrent, Key-Value Stores (Arvind Arasu, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Aymeric Fromherz, Kesha Hietala, Bryan Parno and Ravi Ramamurthy), In Certified Programs and Proofs, 2023. |
| [7] | Modularity, Code Specialization, and Zero-Cost Abstractions for Program Verification (Ho, Son, Fromherz, Aymeric and Protzenko, Jonathan), In Proc. ACM Program. Lang., Association for Computing Machinery, volume 7, 2023. |
| [6] | Verifying Indistinguishability of Privacy-Preserving Protocols (Linvill, Kirby, Kaki, Gowtham and Wustrow, Eric), In Proc. ACM Program. Lang., Association for Computing Machinery, volume 7, 2023. |
|
| [5] | Pipit on the Post: Proving Pre- and Post-Conditions of Reactive Systems (Amos Robinson and Alex Potanin), In 38th European Conference on Object-Oriented Programming, ECOOP 2024, September 16-20, 2024, Vienna, Austria (Jonathan Aldrich, Guido Salvaneschi, eds.), Schloss Dagstuhl - Leibniz-Zentrum für Informatik, volume 313, 2024. |
| [4] | StarMalloc: A Formally Verified, Concurrent, Performant, and Security-Oriented Memory Allocator (Antonin Reitz, Aymeric Fromherz and Jonathan Protzenko), In CoRR, volume abs/2403.09435, 2024. |
| [3] | Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming (Saikat Chakraborty, Gabriel Ebner, Siddharth Bhat, Sarah Fakhoury, Sakina Fatima, Shuvendu K. Lahiri and Nikhil Swamy), In CoRR, volume abs/2405.01787, 2024. |
| [2] | 3DGen: AI-Assisted Generation of Provably Correct Binary Format Parsers (Sarah Fakhoury, Markus Kuppe, Shuvendu K. Lahiri, Tahina Ramananandro and Nikhil Swamy), 2024. |
| [1] | Securing Verified IO Programs Against Unverified Code in F* (Andrici, Cezar-Constantin, Ciobâc\ua, undefinedtefan and Hri\ctcu, C\uat\ualin, Martínez, Guido, Rivas, Exequiel, Tanter, Éric and Winterhalter, Théo), In Proc. ACM Program. Lang., Association for Computing Machinery, volume 8, 2024. |
