Robert Zhang

Scholar, Twitter, GitHub, LinkedIn
robertz@cs.utexas.edu
robert-portrait

News
[Apr. 3, 2026] Optimal Predicate Pushdown Synthesis and MatchBox: A Semantic Foundation for Data Plane Portability have been accepted to PLDI 2026! 🎉
[Jan. 25, 2026] Terminal-Bench: Benchmarking Agents on Hard, Realistic Tasks in Command Line Interfaces has been accepted to ICLR 2026! 🎉
[Jul. 10, 2025] CRUST-Bench: A Comprehensive Benchmark for C-to-safe-Rust Transpilation has been accepted to COLM 2025 as a spotlight! 🎉
[Oct. 21, 2024] I'll present our OOPSLA 2024 paper at SPLASH on Wednesday Oct. 23 at 10:40 am PT
[Sept. 18, 2024] Our OOPSLA 2024 work has been spotlighted on the Johns Hopkins CS department website
[Dec. 22, 2023] Our paper A Pure Demand Operational Semantics with Applications to Program Analysis has been accepted to appear at OOPSLA 2024! 🎉
[Aug. 23, 2023] I'm honored to have been selected as the 2023 Masson Fellow
[May 1, 2023] I'll be volunteering at PLDI 2023 and attending OPLSS

I'm a Computer Science PhD student at the University of Texas at Austin, where I work on program verification & synthesis.

Previously, I did my undergrad and master's at Johns Hopkins University, where I worked with Prof. Scott Smith on demand-driven program semantics in the Programming Languages Laboratory.

Publications
Ongoing Research

  • Pure Demand Operational Semantics

    A novel minimal-state semantics that uses a "stack trace" to look up variables on demand, driving a more precise, compact, and performant static program analysis that does away with the widening step. It executes programs in one go and derives expressive recurrences as results.

    • Fixed/improved theory and implemented various versions of the interpreter and program analysis in OCaml.
    • Extended program analysis to generate CHCs from analysis results and solve them with Z3 for high control flow path sensitivity and verification of final result.
    • Benchmarked analysis performance against Demand-Driven Program Analysis (backwards) and P4F (forwards).
    • Mechanize the interpreter and program analysis in Coq to formally prove determinism, soundness, the former's equivalence to standard interpreters, etc.
    • Co-authored a paper on our work, which has been accepted to appear at OOPSLA 2024.

  • Compiler-Optimized Atomic Execution in Intermittent Computing

    Upon power loss, instructions in an atomic region must restart together. Ocelot automatically analyzes and transforms Rust code for safe and timely intermittent computation. It leverages a hybrid of atomic execution and JIT checkpointing (saving volatile state right before failure) to enforce memory consistency while ensuring freshness and temporal consistency of non-idempotent inputs (e.g., sensor readings).

    • Revamped project to support LLVM 17 and use the new pass manager. Improved C++ code style and added extensive debug logging.
    • Fixed Ocelot's atomic region inference LLVM pass to (1) exhaustively place instructions tainted by the same input into the same region and (2) fully erase instructions associated with fresh/consistent annotations.
    • Extend pass to cluster input-tainted instructions closer together via instruction scheduling, loop unrolling, and function inlining, yielding smaller atomic regions for lower power consumption and greater forward progress.

  • Coq Elaboration for DCS

    DCS is a practical strong functional programming language driven by a sophisticated type-based termination analysis that allows naturally writing divide-and-conquer programs where recursive calls are permitted on values that are not sub-data of the original inputs (e.g., the two halves of a split list in merge sort). DCS uses subtyping to elide the extensive set of coercions required by type checking. Extends essence of POPL 2023 paper.

    • Set up continuous integration to build the Haskell project on merge/push for higher code quality assurance.
    • Improved DCS' module system through a more usable import mechanism.
    • Introduce type casts based on subtyping relations to make the implicit coercions explicit.
    • Design and implement in Haskell an elaboration process to compile DCS programs (with explicit coercions) into Coq for further assurance of termination and to prove program properties.
Service & Honors

  • Masson Fellow (news article, proposal)

    Established in honor of the Department of Computer Science's inaugural chair, Gerald M. Masson, the fellowship recognizes and supports top students enrolled in the Combined Bachelor's/Master's degree program based on research merit. Sole recipient.

  • Member, Upsilon Pi Epsilon

    Upsilon Pi Epsilon is "the first and only, existing international honor society in the Computing and Information disciplines." Selected from a competitive process as one of the 2023 inductees.

  • Dean's Master's Fellow 2023

    Fellowship covering half of the tuition for every semester of full-time, residential enrollment in the master's degree for students who graduate with a Johns Hopkins University undergraduate degree.

Experience
Teaching
Open Source

  • Author of Lyte: a collection of highly extensible React components.

  • Author of LytePQ: a small and mighty suite of data structures in JavaScript.

  • Creator of trade-ml: a bitcoin trading simulation app implemented in OCaml and ReScript.

  • Co-Founder and CTO of Notest: an AI-enabled question generation note-taking app.

  • Contributor to Modern.js: an open source meta-framework suite.

Older Projects

  • Fractals: A hassle-free all-in-one event planning experience.

  • MyCourses: A light-weight app for searching Johns Hopkins University CS Courses and managing those you took, are taking, and are going to take.

  • BlooChat: A simple yet fluid chatting experience with anyone online.