Markus de Medeiros

About Me

I'm Markus, a PhD student at NYU working with Joseph Tassarotti. Lately, we have been working on the Clutch logic.

I am broadly interested in formal methods. In particular, I am interested in verifying privacy and security properties of randomized systems at a realistic scale.

Previously, I worked on automatically translating type-correctness information from the Rust compiler into an explicit memory safety proofs, as part of the Prusti project with Alex Summers at UBC.

During an internship at AWS in the summer of 2024 I also worked on the SampCert verified differential privacy library.

Publications

See also: [ preprints ]

• • Verified Foundations for Differential Privacy
  • Markus de Medeiros, Muhammad Naveed, Tancrete Lepoint, Temesghen Kahsai, Tristan Ravitch, Stefan Zetzsche, Anjali Joshi, Joseph Tassarotti, Aws Albarghouthi, Jean-Baptiste Tristan
  • To appear in PLDI 2025 [ arXiv ] [ Cryptology ePrint Archive ]
• • Tachis: Higher-Order Separation Logic with Credits for Expected Costs
  • Philipp G. Haselwarter, Kwing Hei Li, Markus de Medeiros, Simon Oddershede Gregersen, Alejandro Aguirre, Joseph Tassarotti, Lars Birkedal
  • OOPSLA 2024 [ DOI ] [ arXiv ]
• • Error Credits: Resourceful Reasoning about Error Bounds for Higher-Order Probabilistic Programs
  • Alejandro Aguirre, Philipp G. Haselwarter, Markus de Medeiros, Kwing Hei Li, Simon Oddershede Gregersen, Joseph Tassarotti, Lars Birkedal
  • ICFP 2024 Distinguished Paper Award [ DOI ] [ arXiv ]
• • Spike Solutions to the Supercritical Fractional Gierer-Meinhardt System
  • Daniel Gomez, Markus de Medeiros, Jun-Cheng Wei, and Wen Yang
  • J. Nonlinear Sci. 2024 [ DOI ]
• • Existence and stability of symmetric and asymmetric patterns for the half-Laplacian Gierer-Meinhardt system in one-dimensional domain
  • Markus de Medeiros, Jun-Cheng Wei, and Wen Yang
  • M3AS 2022 [ DOI ]

Blog Posts

Dog

Here is my cute dog!