1) Wider research context

Formal verification aims to ensure the correctness of complex systems, hardware designs,

and software. Unlike traditional testing methods, which rely on executing test cases, formal

verification analyses and validates system properties using precise mathematical

techniques and logical reasoning. The successful development of sophisticated automated

reasoning tools such as solvers for the boolean satisfiability (SAT) problem and computer algebra

algorithms opened up new perspectives and challenges for formal verification. Although both

SAT and computer algebra have a long history, they have only been utilized for problem solving

separately. Because of the absence of close integration, it is currently not possible to

simultaneously harness the strengths of both worlds for real-world problem solving in a single method.

2) Objectives

The mission of this project is to alter the reasoning landscape in bit-precise formal

verification by developing unique SAT-based algebraic methods for word-level reasoning over

polynomials. We focus on integrating SAT solving into algebraic reasoning over pseudo-boolean

integer polynomials, which are for instance used to verify hardware circuits, as well as

polynomials over finite domains, which can be used to model computer memory and cryptographic

encodings. We additionally develop proof logging techniques to certify the verification results.

3) Approach

The research in this project will follow two directions to achieve the goals:

(1) effective SAT solving for polynomial arithmetic, with a focus on (a) pseudo-boolean integer

polynomials, (b) finite fields, and (c) large words (i.e., bit-vectors); and (2) proof logging. We

extract state-of-the-art SAT paradigms and lift these techniques from propositional reasoning to

computer algebra by generalizing the identified inference algorithms to the selected polynomial

rings. Furthermore, we increase the capacity of algebraic proof calculi by incorporating proof

logging into all developed reasoning processes.

4) Level of innovation

Advancing formal method techniques is indispensable. Tightly linking algebraic reasoning with

SAT solving will enable us to fully exploit the potential of both techniques, and has the potential

to significantly increase the capacity of state-of-the-art methods for reasoning over finite fields,

large words, or pseudo-boolean integer polynomials. The timeliness of the proposed research

cannot be emphasized enough. Success in this project will yield unique theoretical and practical

solutions with practical applications in hardware verification, bit-vector reasoning, blockchain

technology and post-quantum cryptography, all of which are of high academic and industrial interest.

5) Primary researchers involved

Principal Investigator: Dr. Daniela Kaufmann (TU Wien)

Mentor: Prof. Laura Kovács (TU Wien)