Heuristische Graphzerlegung für redundanzarme Pfadbedingungen in ValSoft

In order to check safety-critical software, conventional software analysis methods are not sufficient. Our software analysis system ValSoft uses data flow analysis and deductive methods to find and analyse influences on relavant information pathes within programs. Program Dependence Graphs (PDG) serves us as a basis to compute conservative approximated path conditions, which indicate the circumstances of dependencies between interesting points in the programs. These conditions containded too much logical redundance. We introduce a partial heuristic method to speed up the computing of path conditions and to reduce the redundance clearly. We use in this connection articulation points, folded cycles and a heuristic graph decomposition method.