Path-based Program Analysis
From PUMA Graduiertenkolleg
A frequent idiom of C programmers is to initialize a data-structure only, if it is in deed accessed later. A static analysis which, independent of the condition, checks whether a variable has been initialized before its use, will thus always flag a potential error. For this reason, analyses are needed which assign to program points conditions under which certain dataflow facts hold. Such an analysis naturally results from a combination of techniques for predicate abstraction and classical dataflow analysis.
Besides for checking conditional initialization of variables, this method can, more generally, be applied also to certify the correct usage of APIs. Thus, it can. e.g., be verified that every security critical system call is preceded by a suitable call to an access control routine.