The dissertation focuses on formally verifying arithmetic circuits using algebraic proof techniques. As an intrinsic part of computers and digital systems as well as to avoid errors, digital circuits must work correctly. Formal verification can be used to test the circuit’s correct specification but when it comes to arithmetic circuits, this can be fairly challenging. Dr. Daniela Kaufmann’s (Institute of Formal Models and Verification) dissertation focuses on developing a fully automatic verification tool that can be used to verify so-called multipliers.

Presented by the Swiss Informatics Society (SI) together with the Austrian Computer Society (OCG) and the Gesellschaft für Informatik (GI), the GI Dissertation Award is accompanied with € 5,000 in prize money and is awarded to outstanding doctoral theses.