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
-
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.
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)