[24] | 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. |
[23] | 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. |
[22] | Towards a Provably Correct Encoding from F* to SMT (Alejandro Aguirre), Inria Internship Report, 2016. |
[21] | 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. |
[20] | 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. |
[19] | 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. |
[18] | 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. |
[17] | 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. |
[16] | 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. |
[15] | 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. |
[14] | 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. |
[13] | 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. |
[12] | The Next 700 Relational Program Logics (Kenji Maillard, Catalin Hritcu, Exequiel Rivas and Antoine Van Muylder), arXiv:1907.05244, 2019. |
[11] | 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. |
[10] | 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. |
[9] | 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. |
[8] | A Security Model and Fully Verified Implementation for the IETF QUIC Record Layer (Delignat-Lavaud, Antoine, Fournet, Cedric, Parno, Bryan, Protzenko, Jonathan, Ramananandro, Tahina, Bosamiya, Jay, Lallemand, Joseph, Rakotonirina, Itsaka and Zhou, Yi), In Proceedings of the IEEE Symposium on Security and Privacy, 2021. |
[7] | Programming and Proving with Indexed Effects (Aseem Rastogi, Guido Martínez, Aymeric Fromherz, Tahina Ramananandro and Nikhil Swamy), 2021. |
[6] | 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. |
[5] | 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. |
[4] | 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. |
[3] | Provably-Safe Multilingual Software Sandboxing using WebAssembly (Bosamiya, Jay, Lim, Wen Shih and Parno, Bryan), In Proceedings of the USENIX Security Symposium, 2022. |
[2] | 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. |
[1] | ASN1*: Provably Correct Non-Malleable Parsing for ASN.1 DER (Haobin Ni, Antoine Delignat-Lavaud, Cédric Fournet, Tahina Ramananandro and Nikhil Swamy), In Certified Programs and Proofs, 2023. |