[24] | ASN1*: Provably Correct Non-Malleable Parsing for ASN.1 DER (Haobin Ni, Antoine Delignat-Lavaud, Cédric Fournet, Tahina Ramananandro, Nikhil Swamy), In Certified Programs and Proofs, 2023. |

[23] | FastVer2: A Provably Correct Monitor for Concurrent, Key-Value Stores (Arvind Arasu, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Aymeric Fromherz, Kesha Hietala, Bryan Parno, Ravi Ramamurthy), In Certified Programs and Proofs, 2023. |

[22] | Provably-Safe Multilingual Software Sandboxing using WebAssembly (Jay Bosamiya, Wen Shih Lim, Bryan Parno), In Proceedings of the USENIX Security Symposium, 2022. |

[21] | 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, 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. |

[20] | Steel: Proof-oriented Programming in a Dependently Typed Concurrent Separation Logic (Aymeric Fromherz, Aseem Rastogi, Nikhil Swamy, Sydney Gibson, Guido Martínez, Denis Merigoux, Tahina Ramananandro), In 25th ACM SIGPLAN International Conference on Functional Programming (ICFP), 2021. |

[19] | DICE*: A Formally Verified Implementation of DICE Measured Boot (Zhe Tao, Aseem Rastogi, Naman Gupta, Kapil Vaswani, Aditya V. Thakur), In 30th Usenix Security Symposium, 2021. |

[18] | Programming and Proving with Indexed Effects (Aseem Rastogi, Guido Martínez, Aymeric Fromherz, Tahina Ramananandro, Nikhil Swamy), 2021. |

[17] | A Security Model and Fully Verified Implementation for the IETF QUIC Record Layer (Antoine Delignat-Lavaud, Cedric Fournet, Bryan Parno, Jonathan Protzenko, Tahina Ramananandro, Jay Bosamiya, Joseph Lallemand, Itsaka Rakotonirina, Yi Zhou), In Proceedings of the IEEE Symposium on Security and Privacy, 2021. |

[16] | SteelCore: An Extensible Concurrent Separation Logic for Effectful Dependently Typed Programs (Nikhil Swamy, Aseem Rastogi, Aymeric Fromherz, Denis Merigoux, Danel Ahman, Guido Martínez), In 25th ACM SIGPLAN International Conference on Functional Programming (ICFP), 2020. |

[15] | Verified Transformations and Hoare Logic: Beautiful Proofs for Ugly Assembly Language (Jay Bosamiya, Sydney Gibson, Yao Li, Bryan Parno, Chris Hawblitzel), In Proceedings of the Conference on Verified Software: Theories, Tools, and Experiments (VSTTE), 2020. |

[14] | Dijkstra Monads for All (Kenji Maillard, Danel Ahman, Robert Atkey, Guido Martínez, Catalin Hritcu, Exequiel Rivas, Éric Tanter), In 24th ACM SIGPLAN International Conference on Functional Programming (ICFP), 2019. (To Appear) |

[13] | The Next 700 Relational Program Logics (Kenji Maillard, Catalin Hritcu, Exequiel Rivas, Antoine Van Muylder), arXiv:1907.05244, 2019. |

[12] | 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, Nikhil Swamy), In 28th European Symposium on Programming (ESOP), Springer, 2019. |

[11] | Formally Verified Cryptographic Web Applications in WebAssembly (J. Protzenko, B. Beurdouche, D. Merigoux, K. Bhargavan), In 2019 IEEE Symposium on Security and Privacy (SP), 2019. |

[10] | Wys*: A DSL for Verified Secure Multi-party Computations (Aseem Rastogi, Nikhil Swamy, Michael Hicks), In 8th International Conference on Principles of Security and Trust (POST) (Flemming Nielson, David Sands, eds.), Springer, volume 11426, 2019. |

[9] | A Verified, Efficient Embedding of a Verifiable Assembly Language (Aymeric Fromherz, Nick Giannarakis, Chris Hawblitzel, Bryan Parno, Aseem Rastogi, Nikhil Swamy), In PACMPL, 2019. |

[8] | Recalling a Witness: Foundations and Applications of Monotonic State (Danel Ahman, Cédric Fournet, Catalin Hritcu, Kenji Maillard, Aseem Rastogi, Nikhil Swamy), In PACMPL, volume 2, 2018. |

[7] | 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, Nikhil Swamy, Santiago Zanella-Béguelin), In The 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2018. |

[6] | 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, Nikhil Swamy), In PACMPL, volume 1, 2017. |

[5] | 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, Jean-Karim Zinzindohoué), In 2nd Summit on Advances in Programming Languages, 2017. |

[4] | Dijkstra Monads for Free (Danel Ahman, Catalin Hritcu, Kenji Maillard, Guido Martínez, Gordon Plotkin, Jonathan Protzenko, Aseem Rastogi, Nikhil Swamy), In 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), ACM, 2017. |

[3] | Towards a Provably Correct Encoding from F* to SMT (Alejandro Aguirre), Inria Internship Report, 2016. |

[2] | 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, Jean-Karim Zinzindohoué, Santiago Zanella-Béguelin), In 43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), ACM, 2016. |

[1] | Verifying Higher-order Programs with the Dijkstra Monad (Nikhil Swamy, Joel Weinberger, Cole Schlesinger, Juan Chen, Benjamin Livshits), In Proceedings of the 34th annual ACM SIGPLAN conference on Programming Language Design and Implementation, 2013. |