New York und Saarbrücken, 11. Mai 2022 — ACM, die Association for Computing Machinery, hat heute die Empfänger des renommierten ACM Software System Award bekanntgegeben.
Der ACM Software System Award ist eine jährliche Auszeichnung, die an Personen oder Organisationen verliehen wird, die sich auf dem Gebiet der Software-System-Entwicklung besonders verdient gemacht haben. In der Vergangenheit wurde der Preis z. B. für die Entwicklung des Unix-Betriebssystems und des World Wide Web verliehen.
Der diesjährige Preis geht an die Entwickler von CompCert, des ersten nutzbaren optimierenden Compilers, für den ein vollständiger maschinengestützter Korrektheitsbeweis geführt wurde und der für eine Vielzahl kommerzieller Prozessor-Architekturen verfügbar ist.
Die Empfänger des Preises sind:
- Xavier Leroy, Collège de France;
- Sandrine Blazy, Universität von Rennes 1, IRISA;
- Zaynah Dargaye, Nomadic Labs;
- Jacques-Henri Jourdan, CNRS, Laboratoire Méthodes Formelles;
- Michael Schmidt, AbsInt Angewandte Informatik GmbH;
- Bernhard Schommer, Universität des Saarlandes und AbsInt GmbH;
- Jean-Baptiste Tristan, Boston College.
Der CompCert-Compiler, dessen Entwicklung im Jahre 2005 begann, ist der erste formal verifizierte industrietaugliche Compiler für die Programmiersprache C. Er unterstützt eine Vielzahl gängiger Computerarchitekturen, darunter PowerPC, ARM, RISC-V und x86 (32 und 64 Bit).
Mit der Einführung von CompCert wurde gegenüber anderen Compilern ein bahnbrechender Fortschritt erzielt. Dank der formalen Verifikation ist das Problem der Fehlkompilierung nunmehr ausgeschlossen: der von CompCert erzeugte Code verhält sich mathematisch nachweislich genau so, wie es die Semantik des C-Quellprogramms vorgibt.
Ein derartig hoher Vertrauensgrad in die Korrektheit des Kompilierungsprozesses war vor CompCert unerreichbar. Nur mit CompCert können Softwareentwickler den allerhöchsten Anforderungen der striktesten Standards sicher genügen.
Heute wird CompCert als Forschungsprojekt bei INRIA, dem französischen Nationalen Forschungsinstitut für Informatik und Automatisierung, weitergeführt. Die AbsInt GmbH aus Saarbrücken bietet kommerzielle Lizenzen an, leistet technischen Support und trägt aktiv zur Weiterentwicklung des Tools bei.
Akademische Einrichtungen aus der ganzen Welt nutzen CompCert als Ausgangsbasis für weitere Forschung, während kommerzielle Unternehmen es in der Entwicklung sicherheitskritischer Anwendungen einsetzen.
Über AbsInt
AbsInt bietet hochmoderne Entwicklungswerkzeuge für eingebettete Systeme an, mit Schwerpunkt auf Validierung, Verifizierung und Zertifizierung von sicherheitskritischer und sicherheitsrelevanter Software.
Zu den Schlüsselprodukten der Firma gehören neben CompCert statische Analysewerkzeuge zur Überprüfung von Codierrichtlinien, zur Timing- und Stackverbrauchs-Analyse und zur Erkennung kritischer Programmierfehler in C- und C++-Code.
AbsInt wurde 1998 gegründet und ist ein Privatunternehmen mit Sitz in Saarbrücken. Seine Kunden kommen aus mehr als 40 Ländern auf der ganzen Welt und aus den unterschiedlichsten Industriezweigen, einschließlich der Luft- und Raumfahrt, der Automobilindustrie, des Gesundheitswesens und des Energiesektors.
Weitere Informationen finden Sie unter absint.com.
Pressekontakt:
Sylvie Tritz
+49 (681) 38 36 00
tritz[at]absint.com
Über ACM
ACM, die Association for Computing Machinery, ist die weltweit größte Fachgesellschaft für Informatik. Sie vereinigt Lehrende, Forschende und Fachleute der Informatik, um den Dialog anzuregen, Ressourcen auszutauschen und neue Herausforderungen anzugehen.
ACM stärkt die kollektive Stimme des Berufsstandes durch eine starke Führung, die Förderung höchster Standards und die Anerkennung technischer Spitzenleistungen. ACM unterstützt die berufliche Entwicklung ihrer Mitglieder, indem sie Möglichkeiten für lebenslanges Lernen, Karriereentwicklung und professionelles Networking bietet.
Weitere Informationen finden Sie unter acm.org.
Pressekontakt:
Jim Ormond, ACM Communications
+1 212-626-0505
ormond[at]hq.acm.org