Gestählte Java Anwendungen durch Verifikation

Bereits die Verwendung von Java gegenüber unsicheren Sprachen wie C oder C++ verbessert die Qualität und Stabilität vieler Anwendungen erheblich: Klassische Fehler wie Typfehler oder Array Bereichsüberschreitungen ergeben einen Laufzeitfehler an Stelle eines undefinierten Verhaltens, was die Fehlersuche erheblich erleichtert.

Ein ähnlich bedeutender Schritt wie der Wechsel von C nach Java hinsichtlich der Stabilität von Anwendungen ist durch Code Verifikation erreichbar. Somit kann bereits während der Anwendungsentwicklung sicher ausgeschlossen werden, dass gewisse Fehlerklassen in der Anwendung überhaupt auftreten können. Dazu gehören u.a.: Deadlocks, Dangling Pointers, sowie alle Arten von Java Laufzeitfehlern.

Der Vortrag beschreibt die auf Datenflussanalyse basierende Technologie und zeigt, welche Fehlerarten das neue Werkzeug VeriFlux zuverlässig lokalisieren kann. Dabei wird auch beleuchtet, wie sich die jeweiligen unerkannten Fehler im Vergleich unter C, C++ und Java bemerkbar machen würden.