Publications (23)
Wasm/k: Delimited Continuations for WebAssembly
Donald Pinckney, Arjun Guha, Yuriy Brun
WebAssembly is designed to be an alternative to JavaScript that is a safe, portable, and efficient compilation target for a variety of languages. The performance of high-level lang…
Bias, Accuracy, and Trust: Gender-Diverse Perspectives on Large Language Models
Aimen Gaba, Emily Wall, Tejas Ramkumar Babu +3
Large language models (LLMs) are becoming increasingly ubiquitous in our daily lives, but numerous concerns about bias in LLMs exist. This study examines how gender-diverse populat…
Blindspots in Python and Java APIs Result in Vulnerable Code
Yuriy Brun, Tian Lin, Jessie Elise Somerville +2
Blindspots in APIs can cause software engineers to introduce vulnerabilities, but such blindspots are, unfortunately, common. We study the effect APIs with blindspots have on devel…
Baldur: Whole-Proof Generation and Repair with Large Language Models
Emily First, Markus N. Rabe, Talia Ringer +1
Formally verifying software properties is a highly desirable but labor-intensive task. Recent work has developed methods to automate formal verification using proof assistants, suc…
Passport: Improving Automated Formal Verification Using Identifiers
Alex Sanchez-Stern, Emily First, Timothy Zhou +3
Formally verifying system properties is one of the most effective ways of improving system quality, but its high manual effort requirements often render it prohibitively expensive.…
Causal Testing: Finding Defects' Root Causes
Brittany Johnson, Yuriy Brun, Alexandra Meliou
Understanding the root cause of a defect is critical to isolating and repairing buggy behavior. We present Causal Testing, a new method of root-cause analysis that relies on the th…
Programmers Are Poor and Overconfident Judges of LLM-Generated Assertions
Zhanna Kaufman, Yuriy Brun, Adithya Murali +1
Code comprehension and code review are already critically important software engineering tasks, and the rising use of AI code generation tools is only increasing that importance. G…
Your Model Is Unfair, Are You Even Aware? Inverse Relationship Between Comprehension and Trust in Explainability Visualizations of Biased ML Models
Zhanna Kaufman, Madeline Endres, Cindy Xiong Bearfield +1
Systems relying on ML have become ubiquitous, but so has biased behavior within them. Research shows that bias significantly affects stakeholders' trust in systems and how they use…
Better Automatic Program Repair by Using Bug Reports and Tests Together
Manish Motwani, Yuriy Brun
Automated program repair is already deployed in industry, but concerns remain about repair quality. Recent research has shown that one of the main reasons repair tools produce inco…
Formal Foundations of Serverless Computing
Abhinav Jangda, Donald Pinckney, Yuriy Brun +1
Serverless computing (also known as functions as a service) is a new cloud computing abstraction that makes it easier to write robust, large-scale web services. In serverless compu…
QEDCartographer: Automating Formal Verification Using Reward-Free Reinforcement Learning
Alex Sanchez-Stern, Abhishek Varghese, Zhanna Kaufman +3
Formal verification is a promising method for producing reliable software, but the difficulty of manually writing verification proofs severely limits its utility in practice. Recen…
Fairness Testing: Testing Software for Discrimination
Sainyam Galhotra, Yuriy Brun, Alexandra Meliou
This paper defines software fairness and discrimination and develops a testing-based method for measuring if and how much software discriminates, focusing on causality in discrimin…
Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verification
Kyle Thompson, Nuno Saavedra, Pedro Carrott +6
Formal verification using proof assistants, such as Coq, enables the creation of high-quality software. However, the verification process requires significant expertise and manual…
Thinking Forward: Memory-Efficient Federated Finetuning of Language Models
Kunjal Panchal, Nisarg Parikh, Sunav Choudhary +3
Finetuning large language models (LLMs) in federated learning (FL) settings has become increasingly important as it allows resource-constrained devices to finetune a model using pr…
Tortoise: Interactive System Configuration Repair
Aaron Weiss, Arjun Guha, Yuriy Brun
System configuration languages provide powerful abstractions that simplify managing large-scale, networked systems. Thousands of organizations now use configuration languages, such…
Fairkit, Fairkit, on the Wall, Who's the Fairest of Them All? Supporting Data Scientists in Training Fair Models
Brittany Johnson, Jesse Bartola, Rico Angell +4
Modern software relies heavily on data and machine learning, and affects decisions that shape our world. Unfortunately, recent studies have shown that because of biases in data, so…
Memory Savings at What Cost? A Study of Alternatives to Backpropagation
Kunjal Panchal, Sunav Choudhary, Yuriy Brun +1
Forward-mode automatic differentiation (FmAD) and zero-order (ZO) optimization are increasingly proposed as memory-efficient, backpropagation-free alternatives for large language m…
Attack-Resilient Image Watermarking Using Stable Diffusion
Lijun Zhang, Xiao Liu, Antoni Viros Martin +3
Watermarking images is critical for tracking image provenance and proving ownership. With the advent of generative models, such as stable diffusion, that can create fake but realis…
Cobblestone: A Divide-and-Conquer Approach for Automating Formal Verification
Saketh Ram Kasibatla, Arpan Agarwal, Yuriy Brun +3
Formal verification using proof assistants, such as Coq, is an effective way of improving software quality, but requires significant effort and expertise. Machine learning can auto…
My Model is Unfair, Do People Even Care? Visual Design Affects Trust and Perceived Bias in Machine Learning
Aimen Gaba, Zhanna Kaufman, Jason Chueng +4
Machine learning technology has become ubiquitous, but, unfortunately, often exhibits bias. As a consequence, disparate stakeholders need to interact with and make informed decisio…
Enforcing Delayed-Impact Fairness Guarantees
Aline Weber, Blossom Metevier, Yuriy Brun +2
Recent research has shown that seemingly fair machine learning models, when used to inform decisions that have an impact on peoples' lives or well-being (e.g., applications involvi…
Effectiveness of Anonymization in Double-Blind Review
Claire Le Goues, Yuriy Brun, Sven Apel +3
Double-blind review relies on the authors' ability and willingness to effectively anonymize their submissions. We explore anonymization effectiveness at ASE 2016, OOPSLA 2016, and…
Avgust: Automating Usage-Based Test Generation from Videos of App Executions
Yixue Zhao, Saghar Talebipour, Kesina Baral +6
Writing and maintaining UI tests for mobile apps is a time-consuming and tedious task. While decades of research have produced automated approaches for UI test generation, these ap…