Die SAT-Technik ist nach Angaben von Coverity im EDA-Bereich (Electronics Design Application) bereits etabliert. Sie nutzt das mathematische Verfahren der sogenannten Boole'schen Satisfiability und soll damit eine bisher unerreichte Genauigkeit bei der statischen Code-Analyse erreichen. Dazu werden Softwaredefekte mit Hilfe mehrerer SAT-Solver aufgespürt.
Eine Kernkomponente der SAT-Engine von Coverity ist der "False Path Pruning Solver". Mittels der Software DNA-Map übersetzt er jeden möglichen Software-Ausführungspfad in Boole'sche Werte (wahr, falsch) und Operatoren (und, nicht, oder etc.) und prüft diese. In einem Testprojekt mit zwei Millionen Lines of Code lieferte dieses bitgenaue Verfahren laut Coverity 30 Prozent weniger falsche Positive als herkömmliche Technik.
Der False Path Pruning Solver ist der erste, den Coverity für seine Lösung "Prevent SQS" anbietet, im kommenden Jahr sollen zwei weitere Solver dazukommen. Diese sollen dann Code-Behauptungen statisch überprüfen, kritische Fehlerkategorien einschließlich Ganzzahlüberläufe erkennen und mehr Pufferüberläufe aufdecken.
Coverity bietet die neue Version von Prevent SQS mit integriertem False Path Pruning Solver ab sofort für C, C++ und Java an. Der Preis ist projektabhängig. (tc)
