This thesis deals with the automated detection of common software weaknesses in C programs. The approach is selective symbolic execution on the source code level with interpolation based path merging. Interpolation and path merging are used to reduce the necessary computational effort without reduction in bug detection accuracy compared to path coverage, the symbolic execution then achieves error and branch coverage. Interpolation is also used to further reduce the computational effort and to achieve a selectable coverage criterion (e.g., branch coverage), at the expense of false negative detections. The interpolation consists in a removal of constraints from the path constraint. It is shown that the considered algorithms yield an interpolation and coverage hierarchy with respect to subsets of constraints and subsets of program paths, and with respect to the implication of coverage criteria, respectively. Modification of source code is not necessary for analysis. Symbolic execution with Satisfiability Modulo Theories Solver is combined with binary instrumentation to efficiently detect different bug types. The implementation is a plug-in extension to the Eclipse C/C++ development tools and uses a debugger machine interface. It is evaluated by detecting memory access errors, infinite loops, information exposures, dead code and data race conditions in test programs from the Juliet test suite for program analyzers.     «

This thesis deals with the automated detection of common software weaknesses in C programs. The approach is selective symbolic execution on the source code level with interpolation based path merging. Interpolation and path merging are used to reduce the necessary computational effort without reduction in bug detection accuracy compared to path coverage, the symbolic execution then achieves error and branch coverage. Interpolation is also used to further reduce the computational effort and to ac...     »

Die vorliegende Arbeit beschäftigt sich mit der automatischen Erkennung von Fehlern (Common Weaknesses) in C Programmen. Der Ansatz ist eine selektive symbolische Ausführung auf der Quelltext-Ebene mit interpolationsbasierter Pfadverschmelzung. Interpolation und Pfadverschmelzung werden einerseits zur Verringerung der nötigen Rechenleistung ohne Genauigkeitsverlust der Fehlererkennung im Vergleich zu Path Coverage eingesetzt, erzielt wird dann ”Error and Branch Coverage”. Andererseits kann die Interpolation zur Erreichung eines wählbaren Coverage-Kriteriums (z.B. Branch Coverage) angepasst werden, um die nötige Rechenleistung noch weiter zur reduzieren, allerdings bei verminderter Genauigkeit der Erkennung. Die Interpolation besteht in einer Entfernung von Constraints aus dem Pfad-Constraint. Es wird gezeigt, dass die betrachteten Algorithmen eine Interpolations- und Coverage-Hierarchie ergeben, bezüglich Teilmengen von Constraints bzw. Teilmengen von Programmpfaden und Implikation von Coverage-Kriterien. Anpassungen des Quelltextes sind zur Analyse nicht erforderlich. Symbolische Ausführung mit Satisfiability Modulo Theories Solver wird mit Instrumentierung von Binärcode kombiniert, um verschiedene Fehlerarten effizient zu erkennen. Die Implementierung ist eine plug-in Erweiterung der Eclipse C/C++ Development Tools und verwendet ein Debugger Machine Interface. Sie wird mit Testprogrammen der Juliet Suite für Speicherzugriffsfehler, Endlosschleifen, Information Exposures, Dead Code und Race Conditions bewertet.     «

Die vorliegende Arbeit beschäftigt sich mit der automatischen Erkennung von Fehlern (Common Weaknesses) in C Programmen. Der Ansatz ist eine selektive symbolische Ausführung auf der Quelltext-Ebene mit interpolationsbasierter Pfadverschmelzung. Interpolation und Pfadverschmelzung werden einerseits zur Verringerung der nötigen Rechenleistung ohne Genauigkeitsverlust der Fehlererkennung im Vergleich zu Path Coverage eingesetzt, erzielt wird dann ”Error and Branch Coverage”. Andererseits kann die I...     »