Ein Computer übernimmt heutzutage sehr viele Aufgaben in unserem täglichen Leben. Neben dem Smartphone liegen wichtige neue Anwendungen in der Kryptographie oder der Künstlichen Intelligenz. Zentral für die die Berechnungen sind dabei die vier Grundoperationen Addition, Subtraktion, Multiplikation und Division. Im Computer, oder genauer in den Schaltkreisen, müssen jedoch immer neue Architekturen mit möglichst wenig Energieverbrauch für diese Arithmetikoperationen entwickelt werden. Die zentrale Herausforderung dabei ist, ob das Gesamtsystem dann garantiert immer richtig rechnet.

Im Projekt „VerA“ erforscht das Institut für Complex Systems unter Leitung von JKU Prof. Dr. Daniel Große genau diese Frage. Es wird eine vollautomatisierte formale Methodik zum Nachweis der Korrektheit für Multiplizier und Dividierer basierend auf symbolischer Computeralgebra entwickelt. Im Resultat können dann Computerprogramme die Beweisaufgabe übernehmen – anders ist es auch nicht möglich, da Arithmetikschaltkreise aus Millionen von Bauteilen bestehen. Ausgangspunkt des Projektes sind eigene Vorarbeiten welche beispielsweise auf der International Conference on Computer Aided Design (ICCAD), einer der führenden Tagungen auf dem Gebiet des Schaltkreisentwurfs, im November 2018 mit dem Best Paper Award ausgezeichnet wurden.

Das Projekt wird von der Deutschen Forschungsgemeinschaft (DFG) mit mehr als einer halben Million Euro gefördert. Prof. Große hatte das Projekt bereits an der Universität Bremen in Deutschland gestartet und kann dieses nun in Linz fortführen. Es handelt sich um ein gemeinsames Projekt mit Prof. Dr. Rolf Drechsler von der Universität Bremen (Deutschland) und Prof. Dr.-Ing. Christoph Scholl von der Albert-Ludwigs-Universität Freiburg (Deutschland).