49 citations · 102 across the 7 of their papers we have counts for
7 papers
Can Transformers Learn to Solve Problems Recursively?
Shizhuo Dylan Zhang, Curt Tigges, Stella Biderman +2
Neural networks have in recent years shown promise for helping software engineers write programs and even formally verify them. While semantic information plays a crucial part in t…
Getting More out of Large Language Models for Proofs
Shizhuo Dylan Zhang, Talia Ringer, Emily First
Large language models have the potential to simplify formal theorem proving and make it more accessible. But how to get the most out of these models is still an open question. To a…
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…
Long-Term Mentoring for Computer Science Researchers
Emily Ruppel, Sihang Liu, Elba Garza +3
Early in the pandemic, we -- leaders in the research areas of programming languages (PL) and computer architecture (CA) -- realized that we had a problem: the only way to form new…
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.…
Proof Repair across Type Equivalences
Talia Ringer, RanDair Porter, Nathaniel Yazdani +2
We describe a new approach to automatically repairing broken proofs in the Coq proof assistant in response to changes in types. Our approach combines a configurable proof term tran…
QED at Large: A Survey of Engineering of Formally Verified Software
Talia Ringer, Karl Palmskog, Ilya Sergey +2
Development of formal proofs of correctness of programs can increase actual and perceived reliability and facilitate better understanding of program specifications and their underl…