Semantic characterisation of dead control-flow paths

Many program verification, testing and performance prediction techniques rely on analysis of statically-identified control-flow paths. However, some such paths may be ´dead´ because they can never be followed at run time, and should therefore be excluded from analysis. It is shown how the formal semantics of those statements comprising a path provides a sound theoretical foundation for identification of dead paths