Air Force Supports Licata’s Software Verification Project

Dan Licata, assistant professor of computer science, is one of 56 scientists in the country to receive a grant from the U.S. Air Force Office of Scientific Research (AFOSR) through its Young Investigator Research Program. The AFOSR is awarding approximately $20.6 million in grants.

The Young Investigator Research Program is open to scientists and engineers at research institutions across the United States who received PhD or equivalent degrees in the last five years and who show exceptional ability and promise for conducting basic research. Licata, who received a PhD in computer science from Carnegie Mellon University in 2011, will use his grant to study “Software Verification with Directed Type Theory.”

Licata’s proposed work will investigate the foundations of proof assistants, tools that programmers and mathematicians can use to help with their work.

“By using a proof assistant, a programmer can rigorously prove that a program will have good behavior every time it is run, finding errors before the program is deployed and run by the user,” Licata explained. “These tools have been used to verify many large programs and programming language implementations, and in the process many behavioral, efficiency, and security problems have been solved.”

The same tools, he said, also can be used by a mathematician to develop mathematics interactively with the computer, and to formally check that mathematical arguments are correct. This increases confidence in mathematical results and in some cases makes proofs easier to develop.

Licata’s will receive $360,000 over three years. The grant will allow him to hire a postdoc to collaborate on the project. For more information on the Young Investigator Research Program and to view other award recipients see this website.