Program Verification Using Polynomials Over Modular Arithmetic

As program verification has matured as a discipline, so distinct topics have emerged and then developed into thriving sub-disciplines, each with their own language and focus. In Satisfiability Modulo Theories (SMT) solving the focus is on deciding the satisfiability of formulae over predicates (constraints) drawn from a background theory. If a SMT formula encodes the existence of a problematic path through a program, then a model of the formula will expose a fault as demonstrated with a counter-example. In abstract interpretation, on the other hand, the objective is typically to infer invariants for a program so as to demonstrate the absence of a fault. These complementary sub-disciplines do not exist in silos completing against one another: one sub-discipline informs the other. This thesis illustrates how these sub-disciplines cross-fertilise in both directions: presenting a new abstract domain that draws on techniques from SMT solving, namely solving systems of symbolic equations (theory solving). One fundamental operation used in the domain construction applies a propagation technique that suggests how the satisfiability the SMT formulae can be reduced to that of deciding the satisfiability of a compact SAT instance. This leads to a new technique for SMT solving.

Although developed in tandem, for sake of presentation the thesis first addresses the satisfiability of systems of polynomial equations over bit-vectors. Instead of conventional bit-blasting, we exploit word-level inference to translate these systems into non-linear pseudo-boolean constraints. We derive the pseudo-booleans by simulating bit assignments through the addition of (linear) polynomials and applying a strong form of propagation by computing Gröbner bases, which provide an analog of a triangular form for systems of polynomials. By handling bit assignments symbolically, the number of Gröbner basis calculations, along with the number of assignments, is reduced. The final Gröbner basis yields an assignment to the bit-vectors, expressed parametrically in terms of the symbolic bits, together with non-linear pseudo-boolean constraints on the symbolic variables, modulo a power of two. The pseudo-booleans can be solved by translation into classical linear pseudo-boolean constraints (without a modulo) or by encoding them as propositional formulae, for which a novel translation process is described. This aspect of the thesis has a practical bias.

The dual theme of the thesis on abstract domain construction has a theoretical bias. The thesis presents MPAD, the modulo polynomial abstract domain, whose invariants are systems of polynomial equations that hold modulo 2 to the power of ω, where ω is bit-width. MPAD systems over d variables symbolically represent sets of points in d-dimensional space as their solutions, and provide a way of representing and inferring polynomial invariants in the presence of wrap-around arithmetic. The domain operations of MPAD are computed using Gröbner bases, but are founded on a closure operation, mirroring a construction familiar in numeric abstraction. Given an input system of polynomials, and their associated solutions, closure derives a finite polynomial representation of all polynomials that satisfy these solutions. Closure is necessary for faithfully computing join and projection, operations that preserve it. Meet does not maintain closure, hence the need for an algorithm for computing it. Unlike convention polynomial abstraction, MPAD satisfies the ascending chain condition, finessing the need for widening. It also remedies the disparity in handling of equality but not disequality in guards, normally found in numeric abstraction: the structure of MPAD allowing the addition of a single polynomial disequality to be reexpressed using closure and join. We demonstrate that MPAD can derive invariants necessary for verifying the correctness of algorithms which exploit integrality, that were previously out of reach.

As a whole, the thesis makes contributions to SMT solving and abstract interpretation, two complementary themes of program verification, both of which draw on common techniques from algebraic computation, namely Gröbner bases.