Static Analysis Under Non-Deterministic Program Assumptions
Abstract
Static analyses overwhelmingly trade precision for soundness and automation. For this reason, their use-cases are restricted to situations where imprecision isn't prohibitive. In this paper, we propose and specify a static analysis that accepts user-supplied program assumptions that are local to program locations. Such assumptions can be used to counteract imprecision in static analyses, enabling their use in a much wider variety of applications. These assumptions are taken by the analyzer non-deterministically, resulting in a function from sets of accepted assumptions to the resulting analysis under those assumptions. We also demonstrate the utility of such a function in two ways, both of which showcase how it can enable optimization over a search space of assumptions that is otherwise infeasible without the specified analysis.
Cite
@article{arxiv.2602.07324,
title = {Static Analysis Under Non-Deterministic Program Assumptions},
author = {Abdullah H. Rasheed},
journal= {arXiv preprint arXiv:2602.07324},
year = {2026}
}