Loading...

Marianna Rapoport

I’m a Senior Applied Scientist in the Automated Reasoning Group (ARG) at AWS Identity, based in Waterloo, Ontario. We use formal methods and software verification to prove the correctness of AWS’s identity and access services, with a special focus on authorization. In that context, I led the compiler development from Dafny to idiomatic Java and Rust, integrating formally verified components into production code. We recently published these results in our paper Formally Verified Cloud-Scale Authorization at ICSE 2025, which won the ICSE Distinguished Paper Award.

My background is, broadly, in programming languages and software verification. I'm interested in techniques that provide guarantees about program correctness—ideally, before a program is run. In my masters, I worked on static program analysis: algorithms that take as input a program's source code, and a question of interest (such as "does this program leak sensitive user information?"). The static-analysis algorithm then produces an answer to the question, with different degrees of precision.

In my PhD, I worked on type systems. One of my results was the design and type-soundness proof of a subset of Scala that includes full support for path-dependent types and singleton types. The proof took two years and multiple attempts, and I'm still thrilled it all came together.

If you'd like to learn more, feel free to check out my papers below, have a look around my GitHub projects, or get in touch any time.

Also, I love movies. I’ve been tracking everything I’ve watched since I moved to Canada in 2012, using a simple star/no-star system for films, documentaries, and series. If you’re into movies, feel free to get in touch--I'm always excited to exchange movie recommendations.

publications
papers
  • Formally Verified Cloud-Scale Authorization
    Aleks Chakarov, Jaco Geldenhuys, Matthew Heck, Michael Hicks, Samuel Huang, Georges-Axel Jaloyan, Anjali Joshi, K. Rustan M. Leino, Mikael Mayer, Sean McLaughlin, Akhilesh Mritunjai, Clement Pit-Claudel, Sorawee Porncharoenwase, Florian Rabe, Marianna Rapoport, Giles Reger, Cody Roux, Neha Rungta, Robin Salkeld, Matthias Schlaipfer, Daniel Schoepe, Johanna Schwartzentruber, Serdar Tasiran, Aaron Tomb, Emina Torlak, Jean-Baptiste Tristan, Lucas Wagner, Michael Whalen, Remy Willems, Tongtong Xiang, Taejoon Byun, Joshua Cohen, Ruijie Fang, Junyoung Jang, Jakob Rath, Hira Taqdees Syeda, Dominik Wagner, Yongwei Yuan
    ICSE 2025
    Distinguished paper award
    pdf

  • Blame for Null
    Abel Nieto, Marianna Rapoport, Gregor Richards, Ondřej Lhoták
    ECOOP 2020
    pdf | code

  • The Future Is Ours: Prophecy Variables in Separation Logic
    Ralf Jung, Rodolphe Lepigre, Gaurav Parthasarathy, Marianna Rapoport, Amin Timany, Derek Dreyer, Bart Jacobs.
    POPL 2020
    pdf | code

  • A Path To DOT: Formalizing Fully Path-Dependent Types
    Marianna Rapoport, Ondřej Lhoták.
    OOPSLA 2019
    Distinguished artifact award
    pdf | code | talk

  • A Simple Soundness Proof for Dependent Object Types
    Marianna Rapoport, Ifaz Kabir, Paul He, Ondřej Lhoták.
    OOPSLA 2017
    Distinguished artifact award
    pdf | code | talk

  • Mutable WadlerFest DOT
    Marianna Rapoport, Ondřej Lhoták.
    FTfJP 2017
    pdf | code

  • Who You Gonna Call? Analyzing Web Requests in Android Applications
    Marianna Rapoport, Philippe Suter, Erik Wittern, Ondřej Lhoták, Julian Dolby.
    MSR 2017
    pdf | code

  • Type-Based Call Graph Construction Algorithms for Scala
    Karim Ali, Marianna Rapoport, Ondřej Lhoták, Julian Dolby, Frank Tip.
    TOSEM 2015
    pdf | code

  • Precise data-flow analysis in the presence of correlated method calls
    Marianna Rapoport, Ondřej Lhoták, Frank Tip.
    SAS 2015
    Radhia Cousot best young researcher paper award
    pdf | poster | code

  • Constructing Call Graphs of Scala Programs
    Karim Ali, Marianna Rapoport, Ondřej Lhoták, Julian Dolby, Frank Tip.
    ECOOP 2014
    Distinguished artifact award
    pdf | code

technical reports
  • A Path To DOT: Formalizing Fully Path-Dependent Types.
    Marianna Rapoport, Ondřej Lhoták. arXiv: 1904.07298. University of Waterloo, 2019

  • A Simple Soundness Proof for Dependent Object Types.
    Marianna Rapoport, Ifaz Kabir, Paul He, Ondřej Lhoták. arXiv: 1706.03814. University of Waterloo, 2017

  • Mutable WadlerFest DOT.
    Marianna Rapoport, Ondřej Lhoták. arXiv: 1611.07610. University of Waterloo, 2016

theses
  • A Path to DOT: Formalizing Scala with Dependent Object Types.
    PhD thesis, submitted in December 2019
    pdf | proofs

  • Data-flow analysis in the presence of correlated calls.
    Masters thesis, University of Waterloo, 2014
    pdf | code
service
past
blog
This is my blog.
movies
I like movies.
contact
[email protected]