Automatic Abstraction for Congruences: A Story of Beauty and the Beast

Photograph of Andy King

Andy King


Just when we thought that verification was a dead topic, the subject has bounced back with forums such as Verification, Model Checking and Abstract Interpretation (VMCAI) attracting record numbers of submissions. This is because model checking offers push button bug finding whereas abstract interpretation gives push button invariant discovery. This talk concerns an output of work funded by a Royal Society Industrial Fellowship which focuses on deriving invariants from binaries to support white-hats. It explains how bit-level operations can be automatically transformed into operations over matrices of linear congruence equations. By composing the matrices (something that is beautifully simple), the invariants in the binary then just drop-out, giving a way to discover what a program actually does without even running it (a problem that one would initially think to be an utter beast).
Thursday 12th May 2011, 14:00
Far-134 (Video Conferencing Room)
Department of Computer Science