Brun Receives Amazon Research Award for Automated Formal Verification

Professor Yuriy Brun of the UMass Amherst College of Information and Computer Sciences (CICS) is one of 26 recipients of a 2021 Amazon Research Award (ARA), which will fund his research on software formal verification via proof synthesis.

Image

The winning project, “Formal Verification via Language-Modeling-Based Proof Synthesis,” builds on Brun’s previous collaboration with former CICS associate professor Arjun Guha, now at Northeastern University, and CICS doctoral student Emily First, on building language models from already-written software proofs and using those models to automatically synthesize new proofs on demand. The trio released a software package, TacTok, designed to automatically synthesize proofs using Coq, a well-established formal proof management system.

“It’s kind of like programming chat bots, which use language models of existing conversations to synthesize responses to new conversation,” explains Brun. “We learn a model of existing proofs and apply it to synthesize new ones. In a way, this approach works even better for software proofs because we can use the computer to check the proof’s correctness. Unlike a chat bot, our proof-synthesizing software can never be wrong. Sometimes, it won't output a proof at all, but if it does, the proof is guaranteed to be correct.”

According to Brun, he and First will use the ARA grant to improve the language models by varying learning parameters. “What we’ve found is that each variation produces a slightly different model that tries to generate slightly different proofs each time, and may succeed at proving a slightly different set of theorems,” he says. “We expect that this diversity in the learning process, and resultant diversity in the set of models, will prove more theorems than any single model can prove on its own.”

The ARA program offers funds for graduate or postdoctoral researchers and Amazon Web Services promotional credits to support research at academic institutions and non-profit organizations in areas that align with Amazon’s mission.

Brun’s current research focuses on software engineering and systems security, creating techniques to automate improvements in system quality, reliability, privacy, and performance. He has received numerous awards and recognitions, including an NSF CAREER award in 2015 and the IEEE TCSC Young Achiever in Scalable Computing Award in 2013. In 2019, he was elected an ACM Distinguished Member. He joined the CICS faculty in 2012, after working as a postdoctoral fellow at the University of Washington, and was promoted to professor in 2021. He earned his doctorate in computer science from the University of Southern California in 2008.

First is a doctoral student working with Brun in the Laboratory for Software Engineering Research (LASER) at CICS. Her research is at the intersection of software engineering, programming languages, and machine learning, with a specific focus on creating tools to automatically generate proofs of software correctness. She received her bachelor’s in math and computer science from Harvey Mudd College in 2017.