I was reflecting on a comment by Rob Simmons on unsound static analyses:
An analysis that is neither sound nor complete is called pragmatic by Jaspan, as there aren't any theorems to be proved about such an analysis: they can be justified only by their utility in practice.
This is a pretty unsatisfying way to evaluate a static analysis; surely, we can make stronger claims than statistical correlations. Could we, perhaps, show that analyses are sound given some additional assumptions on the program?
Consider the classic example of determining if a variable in a C program is constant. A sound analysis requires a points-to analysis; an unsound analysis requires only a syntactic scan. It seems that it would be straightforward to prove the soundness of this analysis if we also assume that, at every assignment through a pointer, that pointer does not refer to the variable of interest. Such a proof should easily turn into an analysis that also outputs a finite list of assumptions made about specific program points to guarantee its soundness. Indeed, I already see comments on unsound analyses such as "This system is unsound because it assumes the inputs are unaliased," which suggests the theorem that the system is sound if the inputs are unaliased.
A search for "partial soundness" turns up a type theory paper, but no analysis papers. Systems such as CCured that generate dynamic checks upon the failure of the analysis seem related, but I've not seen them interpreted this way. Is there prior work along these lines?