Aseem Rastogi

SteelCore: An Extensible Concurrent Separation Logic for Effectful Dependently Typed Programs

2021 · arXiv (Cornell University)

Much recent research has been devoted to modeling effects within type theory. Building on this work, we observe that effectful type theories can provide a foundation on which to build semantics for more complex programming …

Finding Inductive Loop Invariants using Large Language Models

2023 · arXiv (Cornell University)

Loop invariants are fundamental to reasoning about programs with loops. They establish properties about a given loop's behavior. When they additionally are inductive, they become useful for the task of formal verification that seeks to …

Project Everest: Perspectives from Developing Industrial-Grade High-Assurance Software

2026 · ACM Transactions on Programming Languages and Systems

Project Everest began at Microsoft Research in 2016, aiming to spur research in program verification to produce industrial-grade software. In collaboration with INRIA and Carnegie Mellon University, Project Everest’s goal was to produce drop-in verified …