TITLE: Discovering Congruence Constraints with SAT

PRESENTER: Dr Andy King, http://www.cs.kent.ac.uk/people/staff/amk/, A.M.King@kent.ac.uk

AFFILIATION:University of Kent UK, http://www.cs.kent.ac.uk/

DATE: Monday 29th September 2008

TIME: 14:00:00

PLACE: CSE Seminar Room, Level 1, K17

ABSTRACT:

Solving systems of propositional constraints (SAT-solving) is now so
efficient that it has become fashionable to reformulate program analysis
problems as SAT instances. Usually this is done for speed, but when it
comes to program analysis there is a continuum between the speed of an
analysis and the precision (what it can actually infer). This talk will
show how SAT solving can be applied to improve the *precision* of analyses
that discover congruence constraints, where a constraint is a linear
equality between variables modulo some base which is a power of two.
This last sentence does not contain a typo: we truly really mean improve
precision rather than speed. This bizarre result will be illustrated with
an example that demonstrates how this new approach to analysis can infer
invariants right down to the granularity of the individual bits of program
variables. The talk will include a short demonstration to illustrate the
feasibility of the technique.

BIOGRAPHY OF SPEAKER:

Andy King is a Reader in Program Analysis at the University of Kent in
England. He holds a Royal Society Industrial Fellowship, under which he is
seconded to Portcullis Computer Security Limited, London to develop program
analysis techniques for the security industrial.

Host:

Andrew Verden

Seminar Convenor:

Van Hai Ho