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 the summer of 2024 I also worked on the SampCert verified differential privacy library.
| Title | Updated | Content |
|---|---|---|
| What does iris-lean do? | Nov 17, 2024 | iris |
| BSc. Thesis: Coupled Borrows | Oct 5, 2024 | academics |
| I've been a PhD student for a year. Now what? | Aug 3, 2024 | academics |
| OOPSLA24 Paper: Tachis | July 20, 2024 | announcement |
| ICFP24 Paper: Eris | July 20, 2024 | announcement |
| NESVD Talk: Eris | April 27, 2024 | academics |
| Surviving Your Math Degree | July 14, 2023 | academics |
| Hello World | June 16, 2023 | meta |
Here is my cute dog!
