Isabelle/HOL formalization for 'Verifying a Solver for Mixed Flow-Sensitive Analyses'

Abstract. Mixed flow-sensitive analyses allow balancing efficiency and precision, and provide a convenient description for thread-modular analyses where shared data is analyzed flow-insensitively. The accumulation of flow-insensitive invariants during a flow-sensitive analysis can be readily encapsulated in update rules. In this work, we formalize a generic interface for update rules in Isabelle/HOL, and provide correctness proofs for several implementations of update rules with various widening and narrowing techniques. As hosting solver, we formalize TDside, an extension of the generic top-down solver that utilizes update rules to solve mixed flow-sensitive analysis problems. We establish its partial correctness relative to the update rule interface and thus for all implementations of the interface. To avoid unnecessary and potentially harmful iterations, we propose an algorithmic improvement for TDside. This allows us to verify the optimality of TDside's result—given a precise update rule and that the analysis problem satisfies certain monotonicity assumptions. With this artifact, we provide the proof files accompanying our paper Verifying a Solver for Mixed Flow-Sensitive Analyses. The proofs have been machine-checked with Isabelle2025-2. Please refer to the README for a detailed description of the artifact.