Adam Chlipala - Past Research Students

Postdoc

• Brittany Nkounkou [Summer-Fall 2023]
• Murali Vijayaraghavan (coadvised with Arvind, now a security & formal-methods engineer at Google) [Fall 2013-Fall 2017]
• Joint papers: computer processor verification in Coq and the Kami framework for doing it more smoothly
• C.J. Bell (now an engineer at Meta) [Spring 2014-Spring 2017]
• Joint papers: verified distributed key-value stores in Coq, verified transactional objects in Coq
• Mohsen Lesani (now an associate professor at UC Santa Cruz) [Fall 2014-Summer 2016]
• Joint papers: verified distributed key-value stores in Coq, verified transactional objects in Coq
• Benjamin Delaware (now an assistant professor at Purdue) [Spring 2014-Summer 2016]
• Joint papers: Fiat program-derivation framework in Coq, Narcissus parser deriver for binary formats, proof-generating extraction, Fiat project summary at SNAPL
• Antonis Stampoulis (now a software-engineering consultant) [Fall 2012-Summer 2014]
• Joint paper: Makam functional pearl
• Duckki Oe (now an engineer at Apollo GraphQL) [Fall 2012-Fall 2013]
• Thomas Braibant (now an engineer at Quadrature) [Spring-Summer 2012]
• Joint papers: verifying mini-Bluespec programs in Coq, reflective tactics for separation logic

PhD

• Samuel Gruetter [Fall 2017-Summer 2024] (now a postdoc at ETH Zürich)
• PhD thesis: Techniques for Foundational End-to-End Verification of Systems Stacks
• Joint papers: live verification of C programs in Coq, the verified IoT lightbulb, omnisemantics, RISC-V formal semantics, verifying a software instruction handler, the verified cryptographic garage-door opener
• Thomas Bourgeat (coadvised with Arvind, now an assistant professor at EPFL) [Spring 2016-Fall 2022]
• PhD thesis: Specification and verification of sequential machines in rule-based hardware languages
• Joint papers: the Kôika hardware-description language in Coq, proving strong isolation for enclave hardware, Kôika profiling and debugging tools, RISC-V formal semantics, verifying a software instruction handler
• Andres Erbsen (now a security & formal-methods engineer at Google) [Fall 2015-Fall 2022]
• PhD thesis: Foundational Integration Verification of Diverse Software and Hardware Components
• Master's thesis: Crafting Certified Elliptic Curve Cryptography Implementations in Coq
• Joint papers: Fiat Cryptography, the verified cryptographic garage-door opener, the verified IoT lightbulb, Fiat Cryptography with random search for assembly, omnisemantics, deriving cryptographic-protocol code with coroutines, verified rewriter generator, reification by parametricity, Rupicola proof-generating extraction, RISC-V formal semantics
• Edward Wang (coadvised with Saman Amarasinghe) [Fall 2019-Fall 2022]
• Clément Pit-Claudel (now an assistant professor at EPFL) [Spring 2014-Fall 2021]
• PhD thesis: Relational compilation: Functional-to-imperative code generation for performance-critical applications
• Master's thesis: Compilation Using Correct-by-Construction Program Synthesis
• Joint papers: Rupicola proof-generating extraction, previous round of proof-generating extraction, Kôika profiling and debugging tools, the Kôika hardware-description language in Coq, Fiat program-derivation framework in Coq, Narcissus parser deriver for binary formats, the verified cryptographic garage-door opener, proving strong isolation for enclave hardware, Fiat project summary at SNAPL
• Mirai Ikebuchi (now an assistant professor at Kyoto University) [Spring-Summer 2016, Fall 2017-Fall 2021]
• PhD thesis: Applications of Homological Algebra to Equational Theories
• Joint paper: using Coq to derive first-order code from higher-order, coroutine-based code for cryptographic protocols
• Joonwon Choi (coadvised with Arvind, now a formal-methods engineer at Apple) [Fall 2014-Fall 2020]
• PhD thesis: Structural Design and Proof of Hierarchical Cache-Coherence Protocols
• Master's thesis: An Inlining Approach to Formal Hardware Semantics
• Joint papers: Hemiola cache-coherence framework in Coq, the Kami framework for hardware verification in Coq, the verified IoT lightbulb
• Jason Gross (now a researcher at MIRI) [Summer 2012-Fall 2020]
• PhD thesis: Performance Engineering of Proof-Based Software Systems at Scale
• Master's thesis: An Extensible Framework for Synthesizing Efficient, Verified Parsers
• Joint papers: verified rewriter generator, Fiat Cryptography, reification by parametricity, Fiat Cryptography with random search for assembly, category theory in Coq, Coq bug minimizer, proof-generating extraction, Fiat program-derivation framework in Coq, Fiat project summary at SNAPL
• Jade Philipoom (now a security engineer at zeroRISC) [Fall 2015-Summer 2020]
• Master's thesis: Correct-by-Construction Finite Field Arithmetic in Coq
• Joint papers: Fiat Cryptography, Rupicola proof-generating extraction, the verified cryptographic garage-door opener, verified rewriter generator
• Peng Wang (now an engineer at Google) [Fall 2012-Fall 2018]
• PhD thesis: Type System for Resource Bounds with Type-Preserving Compilation
• Joint papers: TiML language for checking running-time bounds with refinement types, compositional compiler correctness in Bedrock, proof-generating extraction, Fiat project summary at SNAPL
• Benjamin Sherman (previously coadvised with and eventually solely advised by Michael Carbin, now an engineer at Waymo) [Fall 2015-Spring 2018]
• Master's thesis: Making Discrete Decisions Based on Continuous Values
• Joint papers: discrete decision-making for computable real numbers, Kami hardware-verification framework in Coq
• Anders Kaseorg (now an engineer at Zulip) [Fall 2014-Summer 2017]
• Joint paper: verified transactional objects in Coq
• Gregory Malecha (coadvised with Greg Morrisett, now director of formal methods at BedRock Systems) [Fall 2011-Fall 2014]
• PhD thesis: Extensible Proof Engineering in Intensional Type Theory
• Joint papers: automated proofs in Ynot, reflective tactics for separation logic

Master's

• Mahmoud Sobier [Spring 2023-Summer 2024]
• Thesis: Process-Algebra Proofs for Distributed, Message-Passing Cryptographic Code
• Arthur Reiner De Belen [Fall 2022-Summer 2024]
• Thesis: Feasibility of Vector Instruction-Set Semantics Using Abstract Monads
• Gabriel Kammer (now a formal-verification engineer at Intel) [Spring 2022-Fall 2023]
• Thesis: MLVR: Regular Expression-Based Specification for Verified Model Checking of Hardware
• Jason Chen [Spring 2022-Summer 2023]
• Áron Ricardo Perez-Lopez (now a CS PhD student at Stanford) [Spring 2019-Summer 2021]
• Thesis: Puppetmaster: a certified hardware architecture for task parallelism
• Christian Omar Altamirano Modesto (now a CS PhD student at Yale) [Fall 2019-Summer 2021]
• Thesis: Formal Verification of an Implementation of the Roughtime Server
• Zygimantas Straznickas [Summer 2019-Spring 2020]
• Thesis: Towards a Verified First-Stage Bootloader in Coq
• Christopher Shao (now an engineer at Jane Street Capital) [Summer 2016-Spring 2019]
• Thesis: A Framework for Specifying and Formally Verifying Application Security Policies
• Clark Wood (coadvised with Danny Weitzner, now CTO of Boston Cybernetics Institute) [Spring 2018-Spring 2019]
• Thesis: A Formal Methods Safe Harbor
• Joint paper: the verified IoT lightbulb
• Teddy Katz (now an engineer at Google) [Fall 2018-Spring 2019]
• Thesis: Verified Compilation of Abstract Network Policies
• Faye Duxovni [Summer 2014-Spring 2016, Summer 2017-Spring 2018]
• Thesis: Mechanized Proofs That Hardware Is Safe From Timing Attacks
• Joint paper: Fiat project summary at SNAPL
• Asya Bergal (now a senior program associate at Open Philanthropy) [Summer 2016-Spring 2017]
• Raeez Lorgat (now CEO of Persona) [Fall 2015-Spring 2017]
• Robert Sloan (now an engineer at Google) [Spring 2015-Spring 2017]
• Thesis: Constructive Synthesis of Optimized Cryptographic Primitives
• Joint paper: Fiat Cryptography
• Sorawit Suriyakarn (now CTO and cofounder at Band Protocol) [Fall 2014-Spring 2017]
• Thesis: A Framework for Synthesizing Transactional Database Implementations in a Proof Assistant
• Joint paper: Fiat project summary at SNAPL
• Benjamin Barenblat (now an engineer at Google) [Fall 2012-Summer 2013, Summer 2014-Summer 2015]
• Thesis: Memory-Safe Microcontroller Applications with the Bedrock Structured Programming System
• UAP report: Beyond the Demo: Designing and Building a "Real" Ur/Web Application
• Stephan Boyer (now an engineer at Notion) [Spring 2014-Spring 2015]
• Ash Zahlen (now an engineer at Afresh) [Fall 2012-Spring 2014]
• Thesis: Galactic: an Ur/Web Course Management System
• Drew Haven (now an engineer at Metronome) [Spring 2012-Summer 2013]
• Thesis: Automated Proof Checking in Introductory Discrete Mathematics Classes

Undergraduate

• Ritam Nag [Fall 2022-Fall 2024]
• Aneesa Beckford [Spring 2024]
• Nour Massri [Spring 2024]
• Chai Lewgasamsarn [Spring 2023-Spring 2024]
• Yue Chen Li [Winter 2023-Spring 2024]
• Viktor Fukala (now a master's student at ETH Zurich) [Fall 2023]
• Joint paper: live verification of C programs in Coq
• Sarah Mokhtar Abdella [Fall 2023]
• Ali Backour [Fall 2023]
• Michelle Touma [since Fall 2023]
• Samuel Tian [Spring 2022-Spring 2023]
• Joint paper: Fiat Cryptography with random search for assembly
• Mohit Hulse [Winter-Spring 2023]
• Nathan Sheffield [Summer 2022-Summer 2023]
• Vishruti Ganesh (now an engineer at Modulus Labs [Spring 2023]
• Steven Reyes [Fall 2022-Spring 2023]
• Andrew Spears [Fall 2022-Spring 2023]
• Annie Liu [Winter 2023]
• Krit Boonsiriseth [Fall 2021-Fall 2022]
• Andrew Huang [Fall 2022]
• Nathan Xiong [Fall 2022]
• Andreea-Cella Florescu [Fall 2022]
• Alexander Warren (now an engineer at Google) [Fall 2021-Spring 2022]
• Derek Yen (now an engineer at Gridspace) [Summer 2022]
• Livia (Chuyue) Sun (now a CS PhD student at Stanford) [Spring 2021-Spring 2022]
• Joint paper: Fiat Cryptography with random search for assembly
• Ashley Lin (now an engineer at Jane Street Capital) [Fall 2020-Spring 2022]
• Joint paper: the verified cryptographic garage-door opener
• Joshua Lee (now a trader at Jane Street Capital) [Fall 2021]
• Shardul Chiplunkar (now a CS PhD student at EPFL) [Spring 2019-Summer 2020]
• Jessica Shi (now a CS PhD student at Penn) [Summer 2020]
• Jasper Haag (now a formal-methods engineer at BedRock Systems) [Fall 2019-Spring 2020]
• Rachana Madhukara (now an EECS PhD student at MIT) [Fall 2019-Spring 2020]
• Jessie Grosen (now a CS PhD student at CMU) [Fall 2017-Fall 2019]
• Lily Chung (now a CS PhD student at MIT) [Summer 2016, Fall 2017-Summer 2019]
• Thomas Carotti [Fall 2018-Spring 2019]
• Ian Clester (now a music-technology PhD student at Georgia Tech) [Spring 2017-Fall 2018]
• Joint paper: RISC-V formal semantics
• Luke Sciarappa [Summer 2016, Summer 2018]
• Joint paper: discrete decision-making for computable real numbers
• Diego Alonso Roque Montoya (now at Dark Forest Technologies) [Fall 2017-Spring 2018]
• Yinzhan Xu (now a CS PhD student at MIT) [Spring 2017-Spring 2018]
• Nipun Pitimanaaree (now CTO and cofounder of INFINIT) [Spring 2016-Spring 2018]
• Emily Mu (now CTO of Marveri) [Spring-Fall 2017]
• Kritkorn Karntikoon (now a PhD student at Princeton) [Spring 2017]
• Joanna Stadnik [Spring 2017]
• Ziv Scully (now an assistant professor at Cornell) [Spring 2014-Summer 2016]
• Joint paper: automatic insertion of database-query result caching in Ur/Web, as a sound compiler optimization
• Katherine Ye (now a PhD student at CMU) [Summer 2015]
• Joint paper: Fiat project summary at SNAPL
• William Navarre [Summer 2014]
• Jan Polasek (now an engineer at Two Sigma) [Fall 2013-Spring 2014]
• Ryan Kavanagh (now faculty at Université du Québec à Montréal) [Summer 2013]
• Santiago Cuellar (now a researcher at Galois) [Fall 2012-Summer 2013]
• Joint paper: compositional compiler verification with data abstraction
• Michael Kelessoglou (now an engineer at Apple) [Fall 2012-Spring 2013]
• Tony Zhao [Fall 2012-Spring 2013]
• Patrick Hulin (now Deputy Policy Director in Connecticut's Office of the Governor) [Spring-Summer 2012]
• Scott Kovach (now a CS PhD student at Stanford) [Fall 2011]
• Pranjal Vachaspati (now an engineer at Ramp) [Fall 2011]
• Edward Z. Yang (now a research engineer at Meta AI Research) [Fall 2011-Spring 2012]
• UAP report: Academic software reuse, an experience report

Other

• Pratap Singh (now a PhD student at CMU) [Spring-Summer 2022]
• Joint paper: RISC-V formal semantics
• Mathieu Fehr (now a PhD student at Edinburgh) [Spring-Summer 2020]
• David Kaloper Meršinjak (now a PhD student at Cambridge) [Fall 2017]
• Pedro Henrique Azevedo de Amorim (now a postdoc at Oxford) [Spring-Summer 2017]
• Di Wang (now an assistant professor at Peking University) [Fall 2016]
• Joint paper: TiML's type system for running-time bounds
• Mutaamba Maasha [Spring 2014-Spring 2016]
• Daniel Gratzer (now a postdoc at Aarhus) [Summer 2013]
• Thomas Grégoire (now at Eisler Capital) [Summer 2013, Fall 2014]
• Joint paper: verifying stencil-code dependency constraints in Coq
• Anish Dhar (now CEO of Cortex) [Summer 2012]

Legend

UAP was a kind of undergraduate senior final project in MIT EECS.

Master's students listed here are from our MEng program, a "5th-year master's" program for our own undergraduates. This is the only master's program in CS at MIT.