First, Brun Receive ACM SIGSOFT Distinguished Paper Award for Automating Formal Verification
Doctoral student Emily First and Professor Yuriy Brun of the Manning College of Information and Computer Sciences (CICS) at UMass Amherst received a Distinguished Paper Award from the Association for Computing Machinery’s special interest group on software engineering (ACM SIGSOFT) at the 2022 International Conference on Software Engineering in Pittsburgh, PA on May 23.
Their winning paper, “Diversity-Driven Automated Formal Verification,” introduces Diva, their tool to automatically generate proofs for the formal verification of software. Diva is the first to break the one-third barrier in formal verification, fully automatically proving 33.8% of the properties normally proven manually by software engineers, as evaluated by the researchers on a large benchmark of open-source software projects. Diva, funded by the National Science Foundation and an Amazon Research Award, expands on their previous proof synthesis tool TacTok, which was co-created with Arjun Guha, now at Northeastern University.
Formal verification of software—proving that software does exactly what it is supposed to do—is crucial when developing high-stakes systems, like those involved in aerospace or medical equipment, where the outcomes must be 100% correct. This process involves using interactive theorem provers (ITP) such as Coq, which are designed to allow for writing of software and of proofs of theorems about the software. Because writing proofs by hand is often prohibitively difficult, developers sometimes make use of tools like TacTok, or solver-based approaches like CoqHammer, to automatically generate them.
Diva, which stands for Diversity in Verification, learns a diverse set of models of what human-written proofs look like, and then generates new proofs for new software fully automatically using those models “The key to Diva’s success is the diversity of the models,” says Brun. “By varying the learning parameters and data inputs, Diva generates many models. While one model may synthesize one kind of proof, another may synthesize another kind of proof. Together, these models can prove 68% more theorems than our prior tool, TacTok, and 77% more than ASTactic, another state-of-the-art proof synthesis tool.”
Unlike TacTok and ASTactic, which also use existing proofs to learn a model, Diva uses an army-of-models approach, with numerous models attempting to guide proof synthesis for each theorem independently. “We’ve observed that when a model is going to prove a theorem, it often does so early on in its search,” explains First. “To ensure we’re spending computational resources on the right models and proving theorems as quickly as possible, we limit the amount of time each model gets to run before moving on to the next one, cycling back as necessary.”
As the researchers explain, Diva’s cycling approach resulted in a 97% decrease in time required to prove a theorem, on average. Diva contributes to the suite of available tools that automatically generate proofs for the formal verification of software, providing access to an additional 11% of theorems that had not previously been provable by existing tools, according to their analysis of a benchmark over 10,000 theorems.
Diva is open-source and publicly available on GitHub. Brun, together with Talia Ringer, an assistant professor at the University of Illinois Urbana-Champaign, and Alex Sanchez-Stern, a postdoctoral researcher at UMass Amherst, recently received a $1 million grant from the DARPA PEARLS (Proof Engineering, Adaptation, Repair, and Learning for Software) program.
“With the new funding from DARPA, we are leading an effort to improve automated formal verification even more, by learning more-complete models of proofs, improving the proof synthesis process, and applying these ideas to repairing proofs that break when software evolves,” Brun says. “Our project, titled ‘PLATO: Enriched Tactic Prediction Models for Proof Synthesis & Repair’, has already shown that augmenting models with information about identifiers, such as variable names, can further improve proof synthesis.”
First is a doctoral student working with Brun in the Laboratory for Software Engineering Research (LASER) at CICS. Her research lies 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 a bachelor’s in mathematics and computer science from Harvey Mudd College in 2017 and a master’s in computer science from UMass Amherst in 2020.
Brun’s current research focuses on software engineering and systems security, creating techniques to automate improvements in system quality, reliability, 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. He received his doctorate in computer science from the University of Southern California in 2008.