CV

Research Interests

I am interested in cyber physical system (CPS) controller synthesis, and more generally, in formal methods.

Publications

CESAR: Control Envelope Synthesis via Angelic Refinements. Aditi Kabra, Jonathan Laurent, Stefan Mitsch, André Platzer.
TACAS 2024.

Verified Train Controllers for the Federal Railroad Administration Model: Balancing Competing Brake and Track Forces. Aditi Kabra, Stefan Mitsch, André Platzer.
EMSOFT 2022. Best Paper finalist.

Geometry Types for Graphics Programming. Dietrich Geisler, Irene Yoon, Aditi Kabra, Horace He, Yinnon Sanders, Adrian Sampson.
OOPSLA 2020.

Online Verification of Commutativity. Aditi Kabra, Dietrich Geisler, Adrian Sampson.
TAPAS 2020.

Education

Candidate for PhD in Computer Science, Carnegie Mellon University, Pittsburgh, PA, USA

Fall 2020 - present.
Advisors: André Platzer and Stefan Mitsch.

Bachelor of Arts, Cornell University, Ithaca, NY, USA - 2019

magna cum laude in Computer Science
cum laude in Mathematics
cum laude in Physics
with distinction in all subjects.

ISC Board, Lilavatibai Podar High School, Mumbai, Maharashtra, India - 2016

97.75% in ISC Board (Physics/Chemistry/Mathematics/Computer Science)
96.2% in ICSE board

Research

Logical Systems Lab

2020-present

  • Designed and formally verified a train control system for the full US Federal Railway Authority physics model in collaboration with Siemens. (Paper)[assets/train-control-emsoft-preprint.pdf] accepted to EMSOFT 2022.
  • Creating a framework to deductively synthesize formally verified controllers given a specification of the environment, safety contract, and possible action space of a cyber physical system.
  • Designed an algorithm to automatically generate symbolic bounds on differential inequalities, with application in CPS controller verification and synthesis.

Capra, Cornell University

2018-2020

As an undergraduate at Cornell, I was a part of Capra, where I contributed to Gator, a DSL for geometry types, and on an algorithm to efficiently verify the commutativity of diagrams such as those representing the transformation between types.

McMahon Lab, Cornell University

2019

At the McMahon Lab, I worked on understanding the scope and applications of Gaussian Boson Sampling.

CLASSE, Cornell University

2016, 2017

Worked on a project to detect dark photons generated by positron-electron annihilation.

Software Engineering

Software Engineer (IC 2), Microsoft, Redmond, WA

Azure Reserved Instance Team.   January 2020 - August 2020.

Software Engineering Intern, Microsoft, Redmond, WA

Azure Reserved Instances team.   May 2019 - August 2019, May 2018 - August 2018.

Engineering Practicum Intern, Google, Mountain View, CA

Chrome User Metrics Analysis Team.   May 2017 - August 2017.

Teaching

Teaching Assistant, Carnegie Mellon University, Pittsburgh, PA

Software Foundations of Security and Privacy.   Fall 2022.
Logical Foundations of Cyber Physical Systems.   Fall 2021.

Teaching Assistant, Cornell University, Ithaca, NY

Text Mining for History and Literature.   Fall 2019.
Introduction to Algorithms.   Spring 2018, Spring 2019.
Data Structures and Object Oriented Programming.   Spring 2017, Fall 2017.

Service

  • Subreviewed for LICS 2023.
  • Subreviewed for NFM 2023.
  • Member of artifact evaluation committee, ASPLOS 2023.
  • Subreviewed for FM 2022.
  • Subreviewed for ICCPS 2022.
  • Subreviewed for iFM 2022.
  • Member of artifact evaluation committee, ASPLOS 2021.
  • Subreviewed for ICCPS 2021.

Awards