Nikhil Swamy

73 papers A* 19A 8B 5Journal 25Unranked 13
YearRankTypeTitle / Venue / Authors
2026 B ed.
Proceedings of the 15th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2026, Rennes, France, January 12-13, 2026
CPP
Kathrin Stark, Yannick Zakowski, Nikhil Swamy, Nicolas Tabareau
2025 A* conf
3DGen: AI-Assisted Generation of Provably Correct Binary Format Parsers.
ICSE
Sarah Fakhoury, Markus Kuppe, Shuvendu K. Lahiri, Tahina Ramananandro, Nikhil Swamy
2025 J jnl
PulseCore: An Impredicative Concurrent Separation Logic for Dependently Typed Programs.
Proc. ACM Program. Lang.
Gabriel Ebner, Guido Martínez, Aseem Rastogi, Thibault Dardinier, Megan Frisella, Tahina Ramananandro, Nikhil Swamy
2025 A* conf
Secure Parsing and Serializing with Separation Logic Applied to CBOR, CDDL, and COSE.
CCS
Tahina Ramananandro, Gabriel Ebner, Guido Martínez, Nikhil Swamy
2025 J jnl
Secure Parsing and Serializing with Separation Logic Applied to CBOR, CDDL, and COSE.
CoRR
Tahina Ramananandro, Gabriel Ebner, Guido Martínez, Nikhil Swamy
2025 A* conf
Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming.
ICSE
Saikat Chakraborty, Gabriel Ebner, Siddharth Bhat, Sarah Fakhoury, Sakina Fatima, Shuvendu K. Lahiri, Nikhil Swamy
2024 J jnl
3DGen: AI-Assisted Generation of Provably Correct Binary Format Parsers.
CoRR
Sarah Fakhoury, Markus Kuppe, Shuvendu K. Lahiri, Tahina Ramananandro, Nikhil Swamy
2024 J jnl
DiffSpec: Differential Testing with LLMs using Natural Language Specifications and Code Artifacts.
CoRR
Nikitha Rao, Elizabeth Gilbert, Tahina Ramananandro, Nikhil Swamy, Claire Le Goues, Sarah Fakhoury
2024 J jnl
Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming.
CoRR
Saikat Chakraborty, Gabriel Ebner, Siddharth Bhat, Sarah Fakhoury, Sakina Fatima, Shuvendu K. Lahiri, Nikhil Swamy
2023 B conf
ASN1*: Provably Correct, Non-malleable Parsing for ASN.1 DER.
CPP
Haobin Ni, Antoine Delignat-Lavaud, Cédric Fournet, Tahina Ramananandro, Nikhil Swamy
2023 B conf
FastVer2: A Provably Correct Monitor for Concurrent, Key-Value Stores.
CPP
Arvind Arasu, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Aymeric Fromherz, Kesha Hietala, Bryan Parno, Ravi Ramamurthy
2023 — conf
Ranking LLM-Generated Loop Invariants for Program Verification.
EMNLP (Findings)
Saikat Chakraborty, Shuvendu K. Lahiri, Sarah Fakhoury, Akash Lal, Madanlal Musuvathi, Aseem Rastogi, Aditya Senthilnathan, Rahul Sharma, Nikhil Swamy
2023 J jnl
Ranking LLM-Generated Loop Invariants for Program Verification.
CoRR
Saikat Chakraborty, Shuvendu K. Lahiri, Sarah Fakhoury, Madanlal Musuvathi, Akash Lal, Aseem Rastogi, Aditya Senthilnathan, Rahul Sharma, Nikhil Swamy
2022 A* conf
Hardening attack surfaces with formally proven binary format parsers.
PLDI
Nikhil Swamy, Tahina Ramananandro, Aseem Rastogi, Irina Spiridonova, Haobin Ni, Dmitry Malloy, Juan Vazquez, Michael Tang, Omar Cardona, Arti Gupta
2021 — conf
FastVer: Making Data Integrity a Commodity.
SIGMOD Conference
Arvind Arasu, Badrish Chandramouli, Johannes Gehrke, Esha Ghosh, Donald Kossmann, Jonathan Protzenko, Ravi Ramamurthy, Tahina Ramananandro, Aseem Rastogi, Srinath T. V. Setty, Nikhil Swamy, Alexander van Renen, Min Xu
2021 J jnl
Steel: proof-oriented programming in a dependently typed concurrent separation logic.
Proc. ACM Program. Lang.
Aymeric Fromherz, Aseem Rastogi, Nikhil Swamy, Sydney Gibson, Guido Martínez, Denis Merigoux, Tahina Ramananandro
2021 J jnl
SteelCore: An Extensible Concurrent Separation Logic for Effectful Dependently Typed Programs.
CoRR
Nikhil Swamy, Aseem Rastogi, Aymeric Fromherz, Denis Merigoux, Danel Ahman, Guido Martínez
2020 A* conf
EverCrypt: A Fast, Verified, Cross-Platform Cryptographic Provider.
SP
Jonathan Protzenko, Bryan Parno, Aymeric Fromherz, Chris Hawblitzel, Marina Polubelova, Karthikeyan Bhargavan, Benjamin Beurdouche, Joonwon Choi, Antoine Delignat-Lavaud, Cédric Fournet, Natalia Kulatova, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Christoph M. Wintersteiger, Santiago Zanella-Béguelin
2020 J jnl
SteelCore: an extensible concurrent separation logic for effectful dependently typed programs.
Proc. ACM Program. Lang.
Nikhil Swamy, Aseem Rastogi, Aymeric Fromherz, Denis Merigoux, Danel Ahman, Guido Martínez
2019 J jnl
A verified, efficient embedding of a verifiable assembly language.
Proc. ACM Program. Lang.
Aymeric Fromherz, Nick Giannarakis, Chris Hawblitzel, Bryan Parno, Aseem Rastogi, Nikhil Swamy
2019 J jnl
EverCrypt: A Fast, Verified, Cross-Platform Cryptographic Provider.
IACR Cryptol. ePrint Arch.
Jonathan Protzenko, Bryan Parno, Aymeric Fromherz, Chris Hawblitzel, Marina Polubelova, Karthikeyan Bhargavan, Benjamin Beurdouche, Joonwon Choi, Antoine Delignat-Lavaud, Cédric Fournet, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Christoph M. Wintersteiger, Santiago Zanella-Béguelin
2019 A* conf
EverParse: Verified Secure Zero-Copy Parsers for Authenticated Message Formats.
USENIX Security Symposium
Tahina Ramananandro, Antoine Delignat-Lavaud, Cédric Fournet, Nikhil Swamy, Tej Chajed, Nadim Kobeissi, Jonathan Protzenko
2019 A conf
Meta-F ^\star : Proof Automation with SMT, Tactics, and Metaprograms.
ESOP
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
2019 — conf
Wys*: A DSL for Verified Secure Multi-party Computations.
POST
Aseem Rastogi, Nikhil Swamy, Michael Hicks
2018 B conf
A monadic framework for relational verification: applied to information security, program equivalence, and optimizations.
CPP
Niklas Grimm, Kenji Maillard, Cédric Fournet, Catalin Hritcu, Matteo Maffei, Jonathan Protzenko, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Santiago Zanella-Béguelin
2018 J jnl
Meta-F*: Metaprogramming and Tactics in an Effectful Program Verifier.
CoRR
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
2018 J jnl
Recalling a witness: foundations and applications of monotonic state.
Proc. ACM Program. Lang.
Danel Ahman, Cédric Fournet, Catalin Hritcu, Kenji Maillard, Aseem Rastogi, Nikhil Swamy
2017 J jnl
A Monadic Framework for Relational Verification (Functional Pearl).
CoRR
Niklas Grimm, Kenji Maillard, Cédric Fournet, Catalin Hritcu, Matteo Maffei, Jonathan Protzenko, Aseem Rastogi, Nikhil Swamy, Santiago Zanella-Béguelin
2017 A* conf
Dijkstra monads for free.
POPL
Danel Ahman, Catalin Hritcu, Kenji Maillard, Guido Martínez, Gordon D. Plotkin, Jonathan Protzenko, Aseem Rastogi, Nikhil Swamy
2017 — conf
Everest: Towards a Verified, Drop-in Replacement of HTTPS.
SNAPL
Karthikeyan Bhargavan, Barry Bond, Antoine Delignat-Lavaud, Cédric Fournet, Chris Hawblitzel, Catalin Hritcu, Samin Ishtiaq, Markulf Kohlweiss, K. Rustan M. Leino, Jay R. Lorch, Kenji Maillard, Jianyang Pan, Bryan Parno, Jonathan Protzenko, Tahina Ramananandro, Ashay Rane, Aseem Rastogi, Nikhil Swamy, Laure Thompson, Peng Wang, Santiago Zanella-Béguelin, Jean Karim Zinzindohoue
2017 A* conf
Implementing and Proving the TLS 1.3 Record Layer.
IEEE Symposium on Security and Privacy
Antoine Delignat-Lavaud, Cédric Fournet, Markulf Kohlweiss, Jonathan Protzenko, Aseem Rastogi, Nikhil Swamy, Santiago Zanella-Béguelin, Karthikeyan Bhargavan, Jianyang Pan, Jean Karim Zinzindohoue
2017 J jnl
Recalling a Witness: Foundations and Applications of Monotonic State.
CoRR
Danel Ahman, Cédric Fournet, Catalin Hritcu, Kenji Maillard, Aseem Rastogi, Nikhil Swamy
2017 J jnl
Verified Low-Level Programming Embedded in F
CoRR
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
2017 J jnl
Verified low-level programming embedded in F.
Proc. ACM Program. Lang.
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
2017 J jnl
WYS*: A Verified Language Extension for Secure Multi-party Computations.
CoRR
Aseem Rastogi, Nikhil Swamy, Michael Hicks
2016 A* conf
Dependent types and multi-monadic effects in F.
POPL
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 Zinzindohoue, Santiago Zanella-Béguelin
2016 J jnl
Dijkstra Monads for Free.
CoRR
Danel Ahman, Catalin Hritcu, Guido Martínez, Gordon D. Plotkin, Jonathan Protzenko, Aseem Rastogi, Nikhil Swamy
2016 — conf
Formal Verification of Smart Contracts: Short Paper.
PLAS@CCS
Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Cédric Fournet, Anitha Gollamudi, Georges Gonthier, Nadim Kobeissi, Natalia Kulatova, Aseem Rastogi, Thomas Sibut-Pinote, Nikhil Swamy, Santiago Zanella-Béguelin
2016 J jnl
Implementing and Proving the TLS 1.3 Record Layer.
IACR Cryptol. ePrint Arch.
Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Cédric Fournet, Markulf Kohlweiss, Jianyang Pan, Jonathan Protzenko, Aseem Rastogi, Nikhil Swamy, Santiago Zanella-Béguelin, Jean Karim Zinzindohoue
2015 A* conf
Safe & Efficient Gradual Typing for TypeScript.
POPL
Aseem Rastogi, Nikhil Swamy, Cédric Fournet, Gavin M. Bierman, Panagiotis Vekris
2014 A* conf
Gradual typing embedded securely in JavaScript.
POPL
Nikhil Swamy, Cédric Fournet, Aseem Rastogi, Karthikeyan Bhargavan, Juan Chen, Pierre-Yves Strub, Gavin M. Bierman
2014 J jnl
Modular protections against non-control data attacks.
J. Comput. Secur.
Cole Schlesinger, Karthik Pattabiraman, Nikhil Swamy, David Walker, Benjamin G. Zorn
2014 — conf
Polymonadic Programming.
MSFP
Michael Hicks, Gavin M. Bierman, Nataliya Guts, Daan Leijen, Nikhil Swamy
2014 A* conf
Probabilistic relational verification for cryptographic implementations.
POPL
Gilles Barthe, Cédric Fournet, Benjamin Grégoire, Pierre-Yves Strub, Nikhil Swamy, Santiago Zanella-Béguelin
2013 A* conf
Fully abstract compilation to JavaScript.
POPL
Cédric Fournet, Nikhil Swamy, Juan Chen, Pierre-Évariste Dagand, Pierre-Yves Strub, Benjamin Livshits
2013 — conf
Increasing human-tool interaction via the web.
PASTE
Thomas Ball, Peli de Halleux, Nikhil Swamy, Daan Leijen
2013 — ed.
Proceedings of the 2013 ACM SIGPLAN Workshop on Programming Languages and Analysis for Security, PLAS 2013, Seattle, WA, USA, June 20, 2013
PLAS
Prasad Naldurg, Nikhil Swamy
2013 J jnl
Secure distributed programming with value-dependent types.
J. Funct. Program.
Nikhil Swamy, Juan Chen, Cédric Fournet, Pierre-Yves Strub, Karthikeyan Bhargavan, Jean Yang
2013 A* conf
Verifying higher-order programs with the dijkstra monad.
PLDI
Nikhil Swamy, Joel Weinberger, Cole Schlesinger, Juan Chen, Benjamin Livshits
2013 — conf
dkal ⋆ : Constructing Executable Specifications of Authorization Protocols.
ESSoS
Jean-Baptiste Jeannin, Guido de Caso, Juan Chen, Yuri Gurevich, Prasad Naldurg, Nikhil Swamy
2012 — ed.
Proceedings of the sixth workshop on Programming Languages meets Program Verification, PLPV 2012, Philadelphia, PA, USA, January 24, 2012
PLPV
Koen Claessen, Nikhil Swamy
2012 A* conf
Self-certification: bootstrapping certified typecheckers in F* with Coq.
POPL
Pierre-Yves Strub, Nikhil Swamy, Cédric Fournet, Juan Chen
2011 A conf
Lightweight monadic programming in ML.
ICFP
Nikhil Swamy, Nataliya Guts, Daan Leijen, Michael Hicks
2011 A conf
Modular Protections against Non-control Data Attacks.
CSF
Cole Schlesinger, Karthik Pattabiraman, Nikhil Swamy, David Walker, Benjamin G. Zorn
2011 A conf
Secure distributed programming with value-dependent types.
ICFP
Nikhil Swamy, Juan Chen, Cédric Fournet, Pierre-Yves Strub, Karthikeyan Bhargavan, Jean Yang
2011 A* conf
Verified Security for Browser Extensions.
IEEE Symposium on Security and Privacy
Arjun Guha, Matthew Fredrikson, Benjamin Livshits, Nikhil Swamy
2011 — conf
Verifying stateful programs with substructural state and hoare types.
PLPV
Johannes Borgström, Juan Chen, Nikhil Swamy
2010 A conf
Enforcing Stateful Authorization and Information Flow Policies in Fine.
ESOP
Nikhil Swamy, Juan Chen, Ravi Chugh
2010 A* conf
Type-preserving compilation of end-to-end verification of security enforcement.
PLDI
Juan Chen, Ravi Chugh, Nikhil Swamy
2009 A conf
A theory of typed coercions and its applications.
ICFP
Nikhil Swamy, Michael W. Hicks, Gavin M. Bierman
2009 — conf
Cross-tier, label-based security enforcement for web applications.
SIGMOD Conference
Brian J. Corcoran, Nikhil Swamy, Michael W. Hicks
2008 A* conf
Fable: A Language for Enforcing User-defined Security Policies.
SP
Nikhil Swamy, Brian J. Corcoran, Michael Hicks
2008 — —
Language-based Enforcement of User-defined Security Policies (As Applied to Multi-tier Web Programs).
Nikhil Swamy
2008 — conf
Verified enforcement of stateful information release policies.
PLAS
Nikhil Swamy, Michael Hicks
2008 J jnl
Verified enforcement of stateful information release policies.
ACM SIGPLAN Notices
Nikhil Swamy, Michael Hicks
2008 A conf
Verified implementations of the information card federated identity-management protocol.
AsiaCCS
Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon, Nikhil Swamy
2007 A* conf
Defeating script injection attacks with browser-enforced embedded policies.
WWW
Trevor Jim, Nikhil Swamy, Michael Hicks
2006 — conf
Managing Policy Updates in Security-Typed Languages.
CSFW
Nikhil Swamy, Michael Hicks, Stephen Tse, Steve Zdancewic
2006 J jnl
Safe manual memory management in Cyclone.
Sci. Comput. Program.
Nikhil Swamy, Michael W. Hicks, Greg Morrisett, Dan Grossman, Trevor Jim
2005 J jnl
Dynamic inference of polymorphic lock types.
Sci. Comput. Program.
James Rose, Nikhil Swamy, Michael Hicks
2004 A conf
Finding and Removing Performance Bottlenecks in Large Systems.
ECOOP
Glenn Ammons, Jong-Deok Choi, Manish Gupta, Nikhil Swamy
2003 — conf
RGL Study in a Hybrid Real-time System.
Neural Networks and Computational Intelligence
Ken Hennacy, Nikhil Swamy, Don Perlis
1999 B conf
Finding a better-than-classical quantum AND/OR algorithm using genetic programming.
CEC
Lee Spector, Howard Barnum, Herbert J. Bernstein, Nikhil Swamy