Symbolic Computation for Mainstream Verification

PI: Budi Arief, Co-I: Andy King, University of Kent

Close integration of symbolic computation with satisfiability modulo theories (SMT) has a lot of potential. A new class of SMT solvers is beginning to emerge that apply powerful algebraic reasoning in the theory component of SMT solvers. Moreover, the gap between what is provided by algebraic reasoning and what is needed for mainstream verification was recently bridged by a novel SMT solver that applies algebraic (Gröbner basis) reasoning over systems of polynomials modulo 2w.

The overarching objective of this work is to migrate symbolic computation into mainstream verification by adapting algebraic reasoning from fields to bit-vectors. Thus far, work at this intersection has focussed on theories with importance in symbolic computation, over the fields of real or complex numbers. But arguably the ring of integers is more important for software verification. To lead in this neglected area, this project will develop Gröbner basis methods that dovetail with the requirements of verification, namely SMT solving and abstract interpretation.