Dyer's research to streamline software verification practices for researchers

With a new grant from the National Science Foundation, Robert Dyer will lead new initiative to help software engineering researchers improve testing and verification practices with advanced automated techniques and tools.

Software engineers use verification tools to search for bugs, maintain high performance, and detect security vulnerabilities. However, the vast number of verification tools available to engineers can make identifying and locating the right ones for a specific project a challenge. It also makes testing so many tools a challenge, as there needs to be realistic test programs to show the tools work.

"Right now people just go find something that looks like a reasonable program, manually put a bug into it, then modify the code to make it fit within the framework so it can actually run," said Dyer, assistant professor in the School of Computing. "It's an entirely ad-hoc process, and it's very tedious and error-prone."

Dyer's proposed project, "Adaptable Realistic Benchmark Generator for Verification (ARG-V)," will streamline that process, eliminating the need to create and inject fake bugs or manually search repositories for compatible code. ARG-V will instead automatically find and convert code repository programs into benchmarks — or verifiers on sample programs — then classify them so they're accessible by search.

"We're trying to automate it so we can find programs that already exist out in the wild that have the properties we're interested in, and then automatically update or modify the programs so they work within this testing framework we have," Dyer said.