We are thrilled to announce that Daniela Kaufmann from our Research Unit Formal Methods in Systems Engineering, has received an ERC Starting Grant for her project POLARIS! The grant is endowed with 1.5 million Euros and is set to run for 5 years.

In today’s digital world, the correctness of computer systems is not optional – it’s essential. From hardware circuits in medical devices and aircraft to cryptographic protocols protecting our data, many systems underpinning modern society have to work exactly as intended. Formal verification uses rigorous mathematical methods and logical reasoning to prove that they do. Daniela Kaufmann is developing new approaches to make this verification more efficient and scalable.

Many verification tasks – including proving hardware correctness, analyzing cryptographic encodings, and reasoning about computer memory – can be represented as non-linear polynomial equations over finite domains. However, satisfiability modulo theory (SMT) solvers typically reduce these problems to reasoning about individual bits. For complex systems involving non-linear arithmetic and many possible states, this quickly becomes prohibitively expensive. Daniela Kaufmann’s research project POLARIS addresses this challenge.

“An SMT solver formulates the logic at the bit level,” Daniela Kaufmann explains. “If, for example, two numbers are multiplied, this multiplication can be translated into logical relationships between the individual bits used to encode those numbers.” The simple operation of multiplication thus becomes an unwieldy system of bit-level relationships, obscuring the original mathematical structure. “We do not completely break down the arithmetic parts of a system into logical statements about individual bits. Instead, we preserve their algebraic structure and represent them as polynomials. We translate the logic of circuits into mathematical expressions that can be manipulated according to the usual rules of algebra.” The algorithms processing these polynomials will be tailored to verification, combining algebraic word-level reasoning with the precision of bit-level methods.

POLARIS aims to develop trustworthy verification techniques that work directly with polynomial representations while retaining bit-level precision. By combining algebraic, word-level reasoning with established bit-level methods, it seeks to verify systems currently considered too complex. Proof logging will produce machine-checkable certificates, allowing results to be independently verified rather than simply trusted. Even if a system has worked correctly for many inputs, it may fail on the next one. “Surprising errors keep turning up,” says Daniela Kaufmann. “Take the famous Pentium bug, for example, which caused Pentium processors in the 1990s to produce incorrect results for certain divisions. Or a recently discovered bug in a Linux kernel that allowed certain users to gain unauthorized root access.” When lives depend on logical systems, mathematical proof is essential to guarantee correct results in every conceivable situation.

“What we need is a tool that can automatically verify the correctness of other systems, and such tools already exist: SMT solvers can automatically determine whether a given logical formula has a solution.” A logical system, such as part of a computer chip, can be translated into a formula and checked by asking: “Is there any possible situation in which this logical formula violates the rules?”. This can be extremely computationally demanding. A crucial part of the approach is independently checkable verification. “It is also important that our method will make it possible to issue a kind of certificate. If our method says, ‘Yes, this chip works correctly,’ this is not simply a verdict that we have to trust. Instead, we obtain a verifiable mathematical answer that proves its correctness.”

POLARIS aims to extend formal verification to complex arithmetic circuits, cryptographic protocols, and low-level memory models. By developing new theoretical foundations and practical algorithms for bit-precise reasoning, the project seeks to make verification more scalable and strengthen the reliability of digital systems.

Congratulations to Daniela on this outstanding achievement!

About Daniela Kaufmann

Daniela Kaufmann is an FWF ESPRIT Fellow and Principal Investigator at the Research Unit Formal Methods in Systems Engineering at TU Wien Informatics. Her research combines computer algebra and automated reasoning to develop scalable verification methods for modern hardware and software systems. By integrating symbolic computation with SAT and SMT solving, she aims to make formal verification more efficient, more powerful, and ultimately more trustworthy. Her work also advances certifying automated reasoning through proof logging, enabling verification results to be independently checked.

She received her PhD in Computer Science from Johannes Kepler University Linz, where her dissertation on the formal verification of arithmetic circuits using computer algebra was awarded the GI Dissertation Award and the Heinz Zemanek Award. She was also recognized with the Generation Future Award for Digitalization and Innovation, presented by teh ORF and Infineon Austria. She actively contributes to the formal methods community as a member of Steering and Program Committees and by serving in leading organizational roles for international conferences and workshops in automated reasoning and formal verification.

Curious about our other news? Subscribe to our news feed, calendar, or newsletter, or follow us on social media.