What does "post-image analysis" mean in the context of formal program analysis? I am reviewing an anonymous paper about a sort of static analysis of programs that uses the phrase "post-image analysis", or "post-image operation" without defining what that is. I am guessing it is a well-known concept in formal methods, even though a Google search has not revealed anything.

I am guessing it means an analysis of the trace of a segment of a program. Basically, you run it a little bit, you collect the trace (perhaps that's a synonym for "image"), and analyse. But I am just guessing.

Can anyone tell me what that is, or give me a pointer?
When working with transition systems,  $\text{post}(s)$ is the set of states that are reachable in a single step from the state $s$; if $S$ is a set of states,

$$\text{post}(S) = \bigcup_{s \in S} \text{post}(S).$$

Also, $\text{post}^*(s)$ is the set of states that are reachable from $s$, i.e., $\text{post}^*$ is the transitive closure of $\text{post}$.