Collaborative Research: SHF: Documentation-Guided Adaptable Static Analysis

Modern software applications are built using frameworks that come with extensive, evolving documentation describing the rules that keep software secure and reliable. However, these rules are scattered across textual descriptions, diagrams, and code examples, making it difficult to determine whether a program complies with them. As a result, rule violations often go undetected until they cause crashes, security vulnerabilities, or performance problems. This project develops approaches that understand the documentation, verify whether software complies with framework guidelines, and help to fix violations. The project's novelties are the automatic translation of informal framework documentation into formal rules and the use of those rules to analyze application code. The project's broader significance includes the potential to improve the reliability, security, and performance of software systems by catching errors early and creating adaptable tools that keep pace as frameworks evolve. The project achieves these goals by developing a methodology that turns scattered framework documentation into formal rules, checks application code against those rules, and explains any violations it finds. First, the project induces formal specifications from multimodal framework documentation, using targeted retrieval and controlled generation to build a model of how a framework behaves and what obligations each program must meet. Second, the project interprets these specifications over application code by combining the framework model with a reachability analysis that reasons selectively about object- and event-dependent behavior and scales without enumerating every execution path. This approach supports several classes of analysis, including witness-based checking, safety violation detection, obligation discharge reasoning, and object-sensitive, demand-driven protocol conformance analysis. Third, the project produces explanations that trace each violation back to the rule and localize the violation to code, enabling targeted guidance for automated repair tools under limited compute budgets. These advancements will improve software debugging and testing workflows and increase the overall safety of digital systems, while training students in program analysis and artificial intelligence. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.