Present
I’m Zain, a PhD student (2023-present) at the University of Pennsylvania,
working with Benjamin C. Pierce on
applying property-based testing techniques to separation logic specifications.
You can try out my work via the cn test subcommand in CN.
I’m interested in bridging the gap between lightweight testing techniques and heavyweight formal verification through property-based testing, fuzzing, and proof automation.
Past
I completed my B.S. degrees at the University of Illinois at Chicago, in Computer Science and, Mathematics and Psychology. During my time there, I worked on various research projects, including:
- Proof automation for separation logic with William Mansky
- Insight problem solving in computer programming with Jennifer Wiley
- Evaluating reproducibility in NLP with Natalie Parde
- Efficient synthesis of chess problems with Andrew Shulman and Evangelos Kobotis
I was a visiting scholar at the Max Planck Institute for Software Systems, working with Deepak Garg on information flow type systems. I also interned as a software engineer at Valkyrie Trading, working on performant multi-threaded code.
Personal
When I’m not programming, I watch movies and listen to music. I also sometimes mess around with creative coding and Photoshop.
Papers
-
Random Testing via Runtime Abstract InterpretationTo appear in OOPSLA 2026 [ABS]Property-based testing of C programs can be automated by synthesizing random input generators from separation-logic specifications. Existing work in this space, like the Bennet testing tool, uses randomized backtracking search, where random values are generated and checked against constraints, backtracking on failure. Although this approach performs well on simple recursive heap structures, it struggles as constraints grow more complex, particularly when they involve pointer arithmetic—as, for example, in the many forms of specialized storage allocators that arise in low-level systems software. Existing work has used targeted optimizations and heuristics to satisfy specific classes of constraints, but this requires continual expansion as new special cases arise, resulting in complex tools. We reframe generation as the iterative refinement of abstract domain elements, where sampling a concrete value is the final refinement. By applying abstract interpretation at runtime to obtain an abstract element, we obtain a lightweight form of constraint solving and propagation that enables randomized testing of programs with complex preconditions. We identify three specific strategies for applying abstract interpretation: (1) speculative refinement, refining abstract elements before sampling based on immediately following constraints, (2) corrective refinement, calculating “desired” abstract elements from information gleaned from failed constraints, and (3) cascading propagation, propagating information from failures to components of compound expressions. We formalize these ideas in a generator DSL whose monadic semantics are parametric over abstract domains. We implement this DSL in Lucas and evaluate it on sixteen workloads: the six original case studies from the Bennet paper, six position-independent data structures, and four free-list allocators. Comparing configurations with and without refinement, we find that refinement finds more bugs in all four allocators and in two of the position-independent data structures—bugs that Bennet-style random backtracking failed to find.
-
Code-Specify-Test-Debug-Prove: Flexibly Integrating Separation Logic Specification into Conventional WorkflowsWe seek to enable more flexible use of rich specifications in a variety of ways that smoothly extend conventional software development practice. We show how a single specification language, based on separation logic to capture the subtle ownership disciplines of systems code, can be used for runtime assertion checking, for property-based testing, and for formal machine-checked proof—and how each of these complements and supports the others. We demonstrate all this on a challenging example: a component of a production hypervisor, running both stand-alone at user level and in situ in the hypervisor.
-
Bennet: Randomized Specification Testing for Heap-Manipulating ProgramsProperty-based testing (PBT), widely used in functional languages and interactive theorem provers, works by randomly generating many inputs to a system under test. While PBT has also seen some use in low-level languages like C, users in this setting must craft all their own generators by hand, rather than letting the tool synthesize most generators automatically from types or logical specifications. For low-level code with complex memory ownership patterns, writing such generators can waste significant amounts of time. CN, a specification and verification framework for C, features a streamlined presentation of separation logic that is specially tuned to present only "easy" logical problems to an underlying constraint solver. Prior work on the Fulminate testing framework has shown that CN’s streamlined specifications can also be checked effectively at run time, providing an oracle for testing whether a memory state satisfies a pre- or postcondition. We show that the restricted syntax of CN is also a good basis for deriving generators for random inputs satisfying separation-logic preconditions. We formalize the semantics for a DSL describing these generators, as well as optimizations that reorder when values are generated and propagate arithmetic constraints. Using this DSL, we implement a property-based testing tool, Bennet, that generates and runs random tests for C functions annotated with CN specifications. We evaluate Bennet on a corpus of programs with CN specifications and show that it can efficiently generate bug-revealing inputs for heap-manipulating programs with complex preconditions.
* Equal contribution
Posters
-
Exploring insight in computer programmingPsychonomics 2023
-
Exploring Restructuring and Aha! in the Context of Computer ProgrammingLab-based research on insight has typically explored solutions on specially designed puzzles, but there is growing interest in exploring insight in more naturalistic contexts. Anecdotally computer programmers report experiences that sound similar to common insight phenomena such as Aha! and restructuring . To better understand moments of insight in computer programming, we conducted a protocol study where we asked intermediate-level computer-programming students to think-aloud as they solved three problems that required non-obvious solutions. Participants began their solutions on a whiteboard and then implemented their solutions in C++. This yielded several data sources including the trace data and the quality of their programmed solutions. This data was used to test whether and when programmers experienced Aha! or restructuring while solving these problems. This data was also used to test whether common findings in insight problem solving research such as the Aha-Accuracy effect and the theorized impasse-insight sequence are present when computer programming.
-
Exploring creative problem solving in the context of computer programmingMPA 2023
Teaching
TA for Penn CIS 5470: Software Analysis (Fall ‘25)
TA for Penn CIS 5000: Software Foundations (Fall ‘24)
TA for UIC CS 361: Systems Programming (Spring ‘23)
TA for UIC CS 377: Ethical Issues in Computing (Fall ‘21, Spring/Fall ‘22, Spring ‘23)
TA for UIC CS 151: Mathematical Foundations of Computing (Fall ‘20, Spring ‘21)