Loading...

Marianna Rapoport

Hi! My name is Marianna and I currently live in Toronto, Ontario, where I'm working as an applied scientist for the automated reasoning group (ARG) at Amazon Web Services (AWS). ARG uses a wide range of formal methods and software verification techniques to ensure, and even mathematically prove, that software behaves as expected.

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. My biggest result 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, written in the Coq theorem prover, took two years and three attempts to finish, and I get still happy every time I think that it actually worked out.

If you want to learn more, check out my projects below or feel free to get in touch. My projects can be found on github and gitlab.

Also, I love movies. If you're looking for recommendations or want to discuss—I've been keeping track of everything I've seen since I moved to Canada, in the Fall of 2012, with binary (star/no star—and even that is hard to keep consistent!) ratings assigned to every movie/documentary/series.

publications
papers
  • Blame for Null
    Abel Nieto, MR, Gregor Richards, Ondřej Lhoták
    ECOOP 2020

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

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

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

  • Mutable WadlerFest DOT.
    MR, Ondřej Lhoták.
    FTfJP 2017
    pdf | proof

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

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

  • Precise data-flow analysis in the presence of correlated method calls.
    MR, 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, MR, 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.
    MR, Ondřej Lhoták. arXiv: 1904.07298. University of Waterloo, 2019

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

  • Mutable WadlerFest DOT.
    MR, 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]