SAT-Engine bildet Software bit-genau ab

Die auf Boolescher Satisfiability (SAT) basierende SAT-Engine integriert den neuartigen False Path Pruning Solver. Diese neue Form der Quellcodeanalyse erstellt eine bit-genaue Repräsentation eines Software-Systems. Jeder mögliche Software-Ausführungspfad wird in Boolesche Werte und Boolesche Operatoren übersetzt und überprüft. Das Verfahren wurde laut Coverty patentiert.

Die bit-genaue Software-Abbildung ermöglicht die Analyse von Quellcode mit Hilfe von auf SAT-Technologie basierten Solvern erstmals im Bereich kommerzieller PC-Programmierung. In einem Testprojekt konnte der False Path Pruning Solver die falsch positiven Ergebnisse um durchschnittlich 30 Prozent reduzieren. Das Projekt umfasste über 2 Millionen Codezeilen aus mehreren Anwendungen von OS-Software.

Coverity plant für 2008 zwei weitere SAT-Solver. Sie sollen Code-Behauptungen statisch überprüfen, kritische Fehlerkategorien erkennen und eine noch größere Anzahl an Buffer Overflows aufdecken. (dsc)