A computer-algebraic approach to formal verification of data-centric low-level software

Methods of Computer Algebra have shown to be useful when formally verifying data-centric hardware designs. This has been demonstrated especially for cases where complex arithmetic computations are tightly coupled with the system's control structures at the bit level. As a consequence of current design trends, however, more and more functionality that was traditionally implemented in hardware is now shifted into the low-level software of the system. Not only control functions but also more and more arithmetic operations and other data-centric functions are involved in this shift. Motivated by this observation, it is the goal of our work to extend the scope of computer-algebraic methods from hardware to low-level software. The paper develops how hardware-dependent software can be modeled algebraically so that efficient proof procedures are possible. Our results show that also in low-level software a computer-algebraic approach can have substantial advantages over state-of-the-art SMT solving.