Tue 22 Oct 2024 12:00 - 12:30 at Pacific C - Proposal Talks Session 1

The theories required for program analysis have evolved past the foundations developed decades ago. Programs display computational effects such as nondeterminism, randomization, exceptions, and mutable state. Orthogonally, bugfinding is often more tangible than establishing correctness.

Specialized techniques have been introduced to handle effects and incorrectness reasoning. While successful, the disjointed nature of those techniques means that new analysis systems must be built to analyze each kind of program and property. In my research, I am creating a logical foundation to consolidate the aforementioned theories, with which I plan to develop a new generation of static analysis tools that are simpler and more efficient than those available today.

I am a PhD Candiate at Cornell University in the area of Logic, Semantics, and Formal Methods, advised by Alexandra Silva. My research focuses on Outcome Logic, a reformulation of Hoare Logic with computational effects at its core. Outcome Logic consolidates the metatheory behind many variants of Hoare Logic, enabling extensible reasoning about different types of programs and tying together ideas developed over that last sixty years including the seminal work of Floyd and Hoare on program logics in the 1960s, extensions of Hoare Logic to nondeterministic and probabilistic programs, monadic effects, and the more recent emphasis on formal methods for incorrectness.

Before coming to Cornell, I worked as a software engineer for six years at Facebook. During that time, I was fortunate to have unique opportunities including using dependently typed Haskell in production, formally verifying concurrent algorithms for an OS microkernel, and experimenting with an information flow control type system for the Hack language. I strive to ground my research in these invaluable experiences.

Tue 22 Oct

Displayed time zone: Pacific Time (US & Canada) change

11:00 - 12:30
Proposal Talks Session 1Doctoral Symposium at Pacific C
11:00
30m
Talk
Full-Stack Collaboration for Robust Heterogeneity-Enabled AI Systems
Doctoral Symposium
Yuxin Qiu University of California at Riverside
11:30
30m
Talk
JMVX: Improving Record-Replay for Managed Languages
Doctoral Symposium
David Schwartz University of Illinois at Chicago
12:00
30m
Talk
Unified Analysis Techniques for Programs with Outcomes
Doctoral Symposium
Noam Zilberstein Cornell University