What does "post-image analysis" mean in the context of formal program analysis?
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}$.