DARPA VSPELLS Award
The HARP lab has won an award, through subcontract with Galois, inc., to work on the DARPA V-SPELLS program: Verified Security and Performance Enhancement of Large Legacy Software. We will be exploring the use of AI-based programming languages for reasoning about code at scale—in the cloud and on supercomputers. This research will directly benefit efforts to repair, update, and formally verify legacy software.
Our group will be collaborating with researchers from Syracuse University, University of Illinois Urbana-Champaign, University of Washington, and Northeastern University, along with those at Galois, to conduct basic research into mostly automatic systems for fortifying large legacy codebases. We will develop methods, tools, and techniques for retrofitting legacy software with new formally verified components written in domain-specific languages.
Our team's focus will be applying our lab's novel approach to analysis of software on interactive modeling and component identification for legacy code, permitting humans to more easily navigate and understand large complex software systems and to identify components for incremental retrofitting. To overcome this challenge we will be applying new AI-based languages we've designed for such tasks. This technology makes us uniquely able to turn high-level and understandable specifications into massively parallel simulations of code that can be run at scale, including on large flexible resources such as cloud systems Amazon EC2, Google Cloud, or Microsoft Azure, and on supercomputers such as UAB Cheaha and even larger US Department of Energy machines, such as ALCF's Theta. Through this project, we are developing the capacity to use understandable specifications and queries to drive interactive state-of-the-art models of very large codebases.