Computers nowadays have taken over a countless number of everyday tasks. In addition to our smartphones, new and important applications include cryptography and artificial intelligence. Key calculation components include four basic operations of addition, subtraction, multiplication, and division. Inside of the computers - more precisely in the circuits - new architectures featuring the lowest possible level of energy consumption have to always be developed in order to perform these arithmetic operations. The core challenge here include guaranteeing that the overall system can always correctly perform the required calculations.

Under the management of Prof. Dr. Daniel Große, a project at the JKU Institute for Complex Systems titled "VerA" is currently exploring this precise question by focusing on developing a fully automated formal methodology to prove the correctness of multipliers and dividers based on symbolic computer algebra. The outcome would mean that computer programs could be able to prove tasks otherwise it is fairly impossible as arithmetic circuits consist of millions of components. The project’s starting point was Prof. Große’s preliminary groundwork which also won a Best Paper Award in November of 2018 at the International Conference on Computer Aided Design (ICCAD), a leading conference in the field of circuit design.

Funded with over half a million euros by the German Research Foundation (DFG), Prof. Große began working on the project at the University of Bremen in Germany and is now continuing the work in Linz. "VerA" is a joint project between Prof. Dr. Rolf Drechsler (University of Bremen, Germany) and Prof. Dr. Ing. Christoph Scholl (Albert Ludwig University of Freiburg, Germany).