Markus de Medeiros

About Me

I'm Markus, a PhD student at NYU working with Joseph Tassarotti. I am broadly interested in formal methods, namely in verifying challenging properties of randomized systems at a realistic scale.

Here are some projects I've worked on:

• Iris-Lean: a port of the Iris logic to the Lean theorem prover.
• Clutch: a family of program logics for verifying properties of randomized programs in Rocq.
• SampCert: a differential privacy library which is verified in Lean and deployed at AWS.
• Prusti: developing an embedding of the Rust type system in a separation logic.

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
  • PLDI 2025 Distinguished Artifact Award [ DOI ] [ 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!