Verification of a Solver for Mixed Flow-Sensitive Analyses in Isabelle

Mixed flow-sensitive analyses allow to balance 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 $\mathrm{TD_{side}}$, 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 $\mathrm{TD_{side}}$. This allows us to verify optimality of $\mathrm{TD_{side}}$'s result—given a precise update rule and that the analysis problem satisfies certain monotonicity assumptions.

Structure and Content

This artifact includes the following files

• proofscripts/
  • Basics_side.thy
  • TD_side.thy
  • TD_side_upd_rule.thy
  • ROOT
• README.md (this file)
• LICENSE.txt

The proofs can be checked on the command line as well as viewed and checked in Isabelle's prover IDE jedit. For a description of the theory (.thy) files, check the section Description of the Theory Files.

How to Run

The theory files have been checked with Isabelle 2025. The interactive theorem prover Isabelle is available for download on the Isabelle homepage. The following subsections describe the steps to check the proofs contained in the directory proofscripts.

Checking the Proofs with Isabelle's Command Line Tool

Run isabelle build -d proofscripts -v TD_side from the artifact's root directory to build the session containing the proofs (this should take approximately 3 minutes).

The expected output when everything runs successfully without an error looks as follows:

Started at <day> <time> 2026
...
[12 lines skipped]
...
Session Unsorted/TD_side
Running TD_side ...
...
[7 lines skipped]
...
TD_side: theory TD_side.Basics_side
TD_side: theory TD_side.TD_side
TD_side: theory TD_side.TD_side_upd_rule
Finished TD_side

Finished at <day> <time> 2026
<timing statistics>

Checking the Proofs with Isabelle's Prover IDE jedit

A theory file can be opened and checked in jedit by running isabelle jedit proofscripts/TD_side_upd_rule.thy from the artifacts root directory.

The bar next to the scrollbar on the right of the file editor view indicates whether a file was successfully processed. A light red color indicates that these parts were not yet checked. To check the entire file, either scroll to the bottom of the file (you will recognize the light red bar following the movement) or open the side tab Theories and check the opened theory. Both methods will trigger the automatic check of the file.

After the file was checked successfully, the bar next to the scrollbar should be plain gray indicating that no error was found. If you find dark red lines in that bar next, then the checking was not successful. The Theories view on the right side shows an overview of checked theories with a similar color highlighting.

The Sidekick tab on the right gives an overview of the structure of a theory file. You can use it to jump to the section or lemma you are interested in.

Overview and Description

Description of the Theory Files

• Basics_side.thy

  This theory defines strategy trees to describe side-effecting equation systems and subtrees of strategy trees for specific prefixes. Additionally, the theory includes definitions for several properties such as (least) partial (post-)solution, monotonic right-hand sides, and the monotonicity of side-effects and dependencies in right-hand sides. The latter three, also termed threefold monotonicity in the accompanying paper, are essential assumptions used for proving the precision of a variant of $\mathrm{TD_{side}}$ with precise updates.

• TD_side.thy

  In this theory, we formalize the top-down solver TD for side-effecting equation systems where side-effects are accumulated using the join operator. We define both the plain, as well as the optimized destabilization mechanism as discussed in the paper. The solver algorithm is then implemented as a parametrized locale, where both versions of the destab function can be used interchangeably. Additionally, the algorithmic improvement needed to prove precision, namely the abort in function eval can be en- or disabled.

  After defining predicates concerning the well-formedness of the stabl set and infl map, we verify the partial correctness of the solver—independent of the destab version used. By additionally enabling the abort mechanism and requiring threefold monotonicity of the equation system, we can then prove that the computed results are precise, i.e., correspond to the least partial post-solution.

• TD_side_upd_rule.thy

  In this theory, we define the interface specifying appropriate update rules for globals. We then implement five of the update rules presented by Stemmler et al. [1] and show that they fulfill the requirements of our interface for update rules. The solver algorithm is implemented with respect to the update rule interface and can be instantiated as needed for different implementations of update_global. Additionally, it implements, for local unknowns, a dynamic detection of widening/narrowing points for which values are accumulated using a combined widening/narrowing operator.

  Once again, the well-formedness of the stabl set and infl map is established as invariant of the solver state. Ultimately, we formally verify the partial correctness of the top-down solver $\mathrm{TD_{side}}$ implementing the generic interface for update rules.

• ROOT

  This file only contains the meta-information on how to build the session and specifies that it includes the TD_side.thy and TD_side_upd_rule.thy theory and the theory files they depend on.

References

[1] Stemmler, F., Schwarz, M., Erhard, J., Tilscher, S., Seidl, H.: Taking out the toxic trash: Recovering precision in mixed flow-sensitive static analyses. Proc. ACM Program. Lang. 9(PLDI) (Jun 2025), https://doi.org/10.1145/3729297