Verifying the Correctness of Bit-twiddling Code

Speaker

Dr. Andy King, University of Kent
Title Verifying the Correctness of Bit-twiddling Code
When 17.12.2008, 14:00 – 15:00,
Where 2002 (Hauptgebäude, Ahornstr. 55)
Abstract The fields of model checking and abstract interpretation are converging: In model checking there is increasing interest in applying abstraction, and in abstract interpretation there is increasing interest in enriching domains so as to support verification. This talk will show how an exotic, and one might even say esoteric abstract domain, promises to be useful when reasoning about the correctness of bit-twiddling code.

The scientific contribution is in showing how SAT solving can be combined with an operation from geometry (affine hull), to express the meaning of a block of code as a system of linear (congruence) equations. These equations can express the wrap-around nature of machine arithmetic, which is necessary when reasoning about the correctness of low-level programs.  The technique will be illustrated with a series of examples.
Biography Andy studied Computer Science and Mathematics at the University of Bath and received his PhD from the University of Southampton in 1992 for his work on compile-time analysis of concurrent logic programs for multiprocessors. He joined the University of Kent in 1994 and has been appointed Reader in Program Analysis in 2007. In the past, most of his research centered on abstract interpretation of logic programs and constraint logic programs. More recently, he has become interested in applying program analysis to problems in security. To name only a few, his work includes contributions to buffer-overrun analysis, polyhedral techniques, termination analysis, and relational analysis of bit-manipulating programs.