Effective typestate verification in the presence of aliasing
Stephen Fink, Eran Yahav, et al.
ISSTA 2006
Static program analysis is concerned with the computation of approximations of the runtime behavior of programs. Precise information about a program's runtime behavior is, in general, uncomputable for various different reasons, and each reason may necessitate making certain approximations in the information computed. This article illustrates one source of difficulty in static analysis of concurrent programs. Specifically, the article shows that an analysis that is simultaneously both context-sensitive and synchronization-sensitive (that is, a context-sensitive analysis that precisely takes into account the constraints on execution order imposed by the synchronization statements in the program) is impossible even for the simplest of analysis problems.
Stephen Fink, Eran Yahav, et al.
ISSTA 2006
G. Ramalingam, Thomas Reps
Theoretical Computer Science
Eran Yahav, G. Ramalingam
PLDI 2004
J. Field, G. Ramalingam
POPL 1995