A researcher in the Florida State University Department of Computer Science has received an Amazon Research Award to develop automated methods to catch software bugs.

Grigory Fedyukovich, an assistant professor of computer science, in the College of Arts and Sciences, has been awarded $60,000 to continue work on automating formal verification of software — the source code analysis of programs to identify bugs or prove the absence of bugs.

While manual verification during software development depends on lengthy hand-written proofs by engineers, automated verification delegates searching to machines. Though automated methods are much less demanding of engineers, they’re currently not quite as efficient.

By investing in automated methods, the time-consuming process of searching proofs is transferred to machines. While this takes the workload off of the engineer, it often takes even more time for a machine to find a proof.

“My research aims to push the boundaries of automation in formal verification, making it computationally less expensive and thus more accessible to software engineers. This will lead to software that is more trustworthy, secure, efficient and safer,” Fedyukovich said.

The methods he’s using are part of automated reasoning, a specialization of artificial intelligence that applies mathematical analysis to understand complex computer systems and large code bases. Unlike artificial intelligence, which is not always 100 percent precise, automated reasoning can guarantee results — instead of solely relying on data, it leverages a definite set of rules that together prove the desired goals. Amazon Web Services is the world’s most broadly adopted cloud platform and is also used to accelerate automated reasoning. Researchers in Amazon’s automated reasoning group use math-based logic to achieve better network security, access management, and reliability for their more than one million customers.

“I was inspired to apply for this award because Amazon Web Services is home to the automated reasoning group, which connects many top-notch researchers in software verification,” Fedyukovich said. “They’re always searching for ways to improve verification processes, and they value fresh ideas.”

Verification is often viewed as a complicated technique with unimpressive execution times, and many software companies are still skeptical about applying verification to their products. Through formal verification, software can be validated to guarantee the absence of certain, if not all, bugs in a particular program.

“Sometimes, research in academia is highly theoretical. Practical applications require more engineering than science and therefore are not published as often. However, Amazon values results that work in practice, even if they are not publishable, and they support this work. It’s becoming more evident that, eventually, many more companies will likely follow this practical philosophy and more actively support our research,” Fedyukovich said.

The Amazon Research Awards were founded in 2015 and merged with the Amazon Web Services Machine Learning Research Awards in 2020. The program offers funds to support research at academic institutions and nonprofit organizations in areas including robotics, machine learning, security, automated reasoning, theorem proving and more. Together, ARA and MLRA have funded research at 150 universities in 28 countries around the world.

“I’m pleased to have been selected for this award because I proposed highly relevant ideas to their mission. I’ve discussed them with several members of Amazon’s automated reasoning group prior to submitting and received positive feedback,” Fedyukovich said.