About me

Hello! I am a postdoctoral research fellow at the University of Michigan working in the lab of Jean-Baptiste Jeannin. My research interests broadly relate to solving problems at the interface of mathematics and computer science. A few of my interests are programming languages, formal methods, intermittent computing, type systems, and logical relation. I want my research to enhance the fidelity of fault-tolerant and safety-critical systems.

Before joining UMich, I completed my PhD in the Computer Science Department at Carnegie Mellon University. I worked with Limin Jia and Farzaneh Derakhshan on guaranteeing the correctness of programs that run intermittently.

Before that, I worked with Jan Hoffmann on quantitative analysis through the CMU REUSE program. We worked on formulating polymorphism for Resource Aware ML, a language capable of inferring tight resource bounds for OCaml programs. This was my introduction to programming languages research.

And before all that, I completed my undergraduate at the University of Kansas where I double-majored in computer science and mathematics, and minored in visual arts (emphasis in painting). While there, I was a research assistant under the guidance of Dr. Suzanne Shontz in scientific computing. I worked on developing quality metrics for high-order meshes for modeling the human heart.

Outside of research, I enjoy oil painting 🎨, running πŸƒπŸ»β€β™€οΈ, cooking πŸ₯Ÿ, gardening πŸͺ΄, exploring πŸ—ΊοΈ, and cat parenting 🐱.

What i'm working on

  • design icon

    Glacier

    The first provably correct supports for concurrent intermittent programs, including a co-designed runtime and type system.

  • Web development icon

    Modal Crash Types

    Crash Types that characterize the logical underpinning of intermittent computing in terms of its key operations -- crash, restore, and commit -- via adjoint logic.

  • mobile app icon

    Usage-Aware proof calculus for dL

    A refinement of dL that statically detects modeling errors in formulae by inspecting their proofs.

Resume

Education

  1. Ph.D., Masters in computer science / Carnegie Mellon University (Computer Science Department)

    2021 β€” 2026

    Studied programming languages and applied logic. My PhD thesis was on the Logical Foundations of Intermittent Computing.

  2. BSc in computer science, BSc in mathematics / University of Kansas

    2017 β€” 2021

    Double majored in computer science and mathematics and minored in painting. I was named the outstanding senior in computer science for my year.

Experience

  1. Teaching Assistant / Carnegie Mellon University

    Fall 2024

    Teaching assistant for Foundations of Security and Privacy, taught by Frank Pfenning.

  2. Teaching Assistant / Carnegie Mellon University

    Spring 2023

    Teaching assistant for Bug Catching: Automated Program Verification, taught by Matt Fredrikson.

  3. Research Intern / REU in Software Engineering at Carnegie Mellon University

    Summer 2020

    Worked on Resource Aware ML with Jan Hoffmann's group.

  4. Undergraduate Research Assistant / University of Kansas

    Fall 2018 - Fall 2020

    Worked on high-order meshing with Suzanne Shontz's group.

  5. Undergraduate Teaching Assistant / University of Kansas

    Fall 2018 - Spring 2020

    TAed Programming I and Programming II, taught by John Gibbons.

  6. Software Engineering Intern / Garmin International, Consumer Automotive (PND)

    Summer 2019

    Developed and tested software for Garmin GPSs.

Publications and Selected Presentations

Logical Foundations of Intermittent Computing (August 2026)
Myra Dotzel
Carnegie Mellon University, Computer Science Department
Thesis Document Thesis Defense Talk
Modal Crash Types for WAR-Aware Intermittent Computing (April 2025)
Myra Dotzel, Farzaneh Derakhshan, Milijana Surbatovich, Limin Jia
ACM TOPLAS
Paper
Intermittent Concurrency (January 2025)
Myra Dotzel, Milijana Surbatovich, Limin Jia
ACM POPL
Poster
Modal Crash Types for Intermittent Computing (November 2024)
Myra Dotzel, Farzaneh Derakhshan, Milijana Surbatovich, Limin Jia
University of Kansas I2S Speaker Series Lawrence, Kansas
Research Talk
Correctness of Intermittent Executions via Modal Crash Types (October 2023)
Myra Dotzel, Farzaneh Derakhshan, Milijana Surbatovich, Limin Jia
Midwest PL Summit 2023 Ann Arbor, Michigan
Research Talk
Modal Crash Types for Intermittent Computing (April 2023)
Farzaneh Derakhshan, Myra Dotzel, Milijana Surbatovich, Limin Jia
ESOP 2023 Paris, France
Paper Technical Report
Assessing Edge Tangling in High-Order Mesh Elements (March 2021)
Myra Dotzel, Suzanne Shontz
SIAM CSE 2021 Virtual

Poster

Untangling High-Order Meshes Based on Signed Angles (October 2019)
Michael Stees, Myra Dotzel, Suzanne Shontz
The 28th IMR Buffalo, NY
Paper
Evaluating Tangling in High-Order Meshes with Tangent Vectors (February 2019)
Myra Dotzel, Michael Stees, Suzanne Shontz
SIAM CSE 2019 Spokane, WA

Research Talk

Awards and Accomplishments

San Francisco Bridge Half Marathon Finisher (July 2026)

National Science Foundation Graduate Research Fellowship (April 2022)
Carnegie Mellon University

2nd place, Logical Foundations of Cyber-Physical Systems Grand Prix (December 2021)
Carnegie Mellon University

Girl Scout Gold Award (January 2015)

Contact

Contact Form