Skip to main content
UMass Collegiate M The University of Massachusetts Amherst
  • Visit
  • Apply
  • Give
  • Search UMass.edu
Manning College of Information & Computer Sciences

Main navigation

  • Academics

    Programs

    Undergraduate Programs Master's Programs Doctoral Program Graduate Certificate Programs

    Academic Support

    Advising Career Development Academic Policies Courses Scholarships and Fellowships
  • Research

    Research

    Research Areas Research Centers & Labs Undergraduate Research Opportunities

    Faculty & Researchers

    Faculty Directory Faculty Achievements

    Engage

    Research News Distinguished Lecturer Series Rising Stars in Computer Science Lecture Series
  • Community

    On-Campus

    Diversity and Inclusion Student Organizations Massenberg Summer STEM Program Awards Programs Senior Celebration

    External

    Alumni Support CICS
  • People
    Full A-Z Directory Faculty Staff
  • About

    Overview

    College Overview Leadership Our New Building

    News & Events

    News & Stories Events Calendar

    Connect

    Visiting CICS Contact Us Employment Offices & Services
  • Info For
    Current Undergraduate Students Current Graduate Students Faculty and Staff Newly Accepted Undergraduate Students

Brun Receives Amazon Research Award for Automated Formal Verification

Content

September 9, 2021
Research
Image
Yuriy Brun
Yuriy Brun

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.

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 nonprofit 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 received 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.

Award or honor posted in Research

Site footer

Manning College of Information & Computer Sciences
  • Find us on Facebook
  • Find us on YouTube
  • Find us on LinkedIn
  • Find us on Instagram
  • Find us on Flickr
  • Find us on Bluesky Social
Address

140 Governors Dr
Amherst, MA 01003
United States

  • Visit CICS
  • Give
  • Contact Us
  • Employment
  • Events Calendar
  • Offices & Services

Info For

  • Current Undergraduate Students
  • Current Graduate Students
  • Faculty & Staff
  • Newly Accepted Undergraduate Students

Global footer

  • ©2025 University of Massachusetts Amherst
  • Site policies
  • Privacy
  • Non-discrimination notice
  • Accessibility
  • Terms of use