Reference 1
Reaching Definition Analysis, (reaching assignment analysis):
An assignment (called a definition in classical literature) of the form $[x:=a]^l$ may reach a certain program point (typically the entry or exit of an elementary block) if there is an execution of the program where $x$ was last assigned a value at $l$ when the program point is reached.
For example, for the factorial program below:
$[y:=x]^1; [z:=1]^2; while [y>1]^3 do ([z:=z*y]^4; [y:=y-1]^5); [y:=0]^6$
we have the following reaching definition analysis result:
$[y:=x]^1$, or $(y,1)$, reaches the program point 2-6.
If you could revise
the fundmental principles of
computer system design
to improve security...
... what would you change?