41 citations · 84 across the 6 of their papers we have counts for
7 papers
Validating AI-Generated Code with Live Programming
Kasra Ferdowsi, Ruanqianqian Huang, Michael B. James +2
AI-powered programming assistants are increasingly gaining popularity, with GitHub Copilot alone used by over a million developers worldwide. These tools are far from perfect, howe…
Retrofitting Fine Grain Isolation in the Firefox Renderer (Extended Version)
Shravan Narayan, Craig Disselkoen, Tal Garfinkel +5
Firefox and other major browsers rely on dozens of third-party libraries to render audio, video, images, and other content. These libraries are a frequent source of vulnerabilities…
Gobi: WebAssembly as a Practical Path to Library Sandboxing
Shravan Narayan, Tal Garfinkel, Sorin Lerner +2
Software based fault isolation (SFI) is a powerful approach to reduce the impact of security vulnerabilities in large C/C++ applications like Firefox and Apache. Unfortunately, pra…
Generating Correctness Proofs with Neural Networks
Alex Sanchez-Stern, Yousef Alhessi, Lawrence Saul +1
Foundational verification allows programmers to build software which has been empirically shown to have high levels of assurance in a variety of important domains. However, the cos…
Targeted Synthesis for Programming with Data Invariants
John Sarracino, Shraddha Barke, Hila Peleg +2
Programmers frequently maintain implicit data invariants, which are relations between different data structures in a program. Traditionally, such invariants are manually enforced a…
Finding Root Causes of Floating Point Error with Herbgrind
Alex Sanchez-Stern, Pavel Panchekha, Sorin Lerner +1
Floating-point arithmetic plays a central role in science, engineering, and finance by enabling developers to approximate real arithmetic. To address numerical issues in large floa…
Equality Saturation: A New Approach to Optimization
Ross Tate, Michael Stepp, Zachary Tatlock +1
Optimizations in a traditional compiler are applied sequentially, with each optimization destructively modifying the program to produce a transformed program that is then passed to…