Verified Security and Performance Enhancement of Large Legacy Software (V-SPELLS)
HR001120S0058
Grants.gov  https://www.grants.gov/web/grants/view-opportunity.html?oppId=328355

The V-SPELLS program will leverage a combination of novel concepts in program understanding and verification, as well as recent developments in domain specific languages and composable system architectures for production systems at scale. The program seeks breakthroughs in and novel approaches to the following technical challenges, Including, but not limited to:
Automated program understanding to infer architectural structure, assumptions, and dependencies in a legacy source code base, enabling its decomposition into components with explicit modular structure, interfaces, dependencies, and constraints. Recovery of domain abstractions and models from legacy code bases, in succinct and expressive representations suitable for programming functional component enhancements or replacements that are safely composable with the existing systems.
Matching known and extracted domain abstractions and models with legacy code, lifting of legacy code to succinct, enhanceable, safely composable, and inter-operating representations, and automated specification inference leveraging such representation. Provably safe composition of enhancements with the rest of the system.
Overcoming performance reduction due to added layers of abstraction with novel verified cross-layer optimization and distribution techniques (“verified stack flattening and distribution”). Development of non-brittle and granular rules for composable representation, packaging, and transformation of software verification proofs that support distribution and orchestration of verified programs.