A formal account of SSA in Java-like languages