Combining Computer Algebra with SAT for Word-Level Reasoning

Formal verification aims to ensure the correctness of complex systems, hardware designs, and software. Unlike traditional testing methods, which rely on executing test cases and observing outputs, formal verification employs precise mathematical techniques and logical reasoning to thoroughly analyze and validate system properties, guaranteeing that they meet specified requirements and standards. Indeed, formal verification is essential in modern engineering practices as it enables the construction of robust and dependable systems that fulfill high quality, safety, and security criteria. The successful development of sophisticated automated reasoning tools such as solvers for the boolean satisfiability problem (SAT) 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 mostly 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. The mission of this project is to alter the reasoning landscape in bit-precise formal verification by combining SAT and computer algebra to develop unique SAT-based algebraic methods for word- level reasoning over polynomials. Here, words describe vectors and sequences of bits, capturing for example, portions of computer memory. However, while discussing the broad area of computer algebra, we have to put our focus on selected polynomial rings. We concentrate 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. To validate the novel methods we additionally develop proof logging techniques to certify the verification results and hence are able to provide an additional layer of trust. Tightly linking algebraic reasoning with SAT solving will enable us to fully harness 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, bit-vectors, or pseudo-boolean integer polynomials. Advancing formal method techniques is indispensable and we believe that linking these orthogonal reasoning approaches is a key step in this direction. 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.