BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//University of Kent/Events Calendar//NONSGML v1.0//EN
BEGIN:VEVENT
UID:44277
DTSTAMP:20200529T150213Z
SUMMARY:PLAS: Andy King
LOCATION:anywhere, via Zoom.
DESCRIPTION:There has been much discussion about how to combine techniques from computer algebra with SMT solving, which is a form of symbolic computation geared towards program verification. We address 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 Groebner bases. By handling bit assignments symbolically, the number of Groebner basis calculations, along with the number of assignments, is reduced. The final Groebner basis yields expressions for the bit-vectors 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.\nWork with Tom Seed and Neil Evans.\n\n
DTSTART:20200608T140000Z
DTEND:20200608T150000Z
URL:
END:VEVENT
END:VCALENDAR