Das von der Forschungsgruppe "Verifikation trifft Algorithmik" entwickelte
Software-Verifikations-Werkzeug LLBMC konnte auf der 2nd International
Competition on Software Verification zwei Gold- und vier Silbermedaillen erringen.

Vom 16.-24. März 2013 trafen sich in Rom Software-Forscher aus aller Welt im Rahmen der European Conference on Theory & Practice of Software (ETAPS 2013).
Die Veranstaltung umfasst neben fünf Hauptkonferenzen und über 20 Workshops
auch die Competition on Software Verification (SV-COMP), die 2013 zum zweiten Mal stattfand.

Gold gewann das Team in den beiden Kategorien BitVectors und Loops.

Bei diesem Wettbewerb treten Programme gegeneinander an, die vollautomatisch
Sofware-Fehler aufspüren können. Diese Software-Verifikations-Werkzeuge erlauben
es, schwer zu findende Programmierfehler systematisch zu identifizieren und die Korrektheit von Programmen zu beweisen, wodurch die Qualität und Zuverlässigkeit von Softwaresystemen deutlich gesteigert werden kann. Verifikationswerkzeuge werden derzeit hauptsächlich in Bereichen eingesetzt, in denen eine hohe Zuverlässigkeit unumgänglich ist, z.B. im Bereich der Luftfahrt und in der Automobilindustrie.

Das am KIT in der Forschungsgruppe "Verifikation trifft Algorithmik" von Stephan Falke und Florian Merz unter Leitung von Carsten Sinz entwickelte System LLBMC zeichnet sich durch hohe Präzision und umfassende Einsetzbarkeit aus.
LLBMC trat in sieben der zehn Kategorien der Competition on Software Verification an und konnte sich in folgenden sechs davon gegen die internationale Konkurrenz behaupten: BitVectors, FeatureChecks, HeapManipulation, Loops, MemorySafety und ProductLines. Dabei setzte sich das Team gegen zehn andere Teams durch, unter anderem aus Russland, Großbritannien, Deutschland und den USA, und errang zwei Gold- und vier Silbermedaillen. Die hohe Präzision von LLBMC zeigte sich auch darin, dass es als einziges Werkzeug in den sieben bearbeiteten Kategorien sämtliche Programmfehler korrekt identifizieren konnte.

Das Gewinnerteam v.l.n.r.: Dr. Carsten Sinz, Florian Merz, Stephan Falke.