Conference Proceedings

Automatic Abstraction for Congruences

A King, H Sondergaard, G Barthe (ed.), M Hermenegildo (ed.)

Lecture Notes in Computer Science: Verification, Model Checking and Abstract Interpretation 11th International Conference, VMCAI | Springer Berlin Heidelberg | Published : 2010


One approach to verifying bit-twiddling algorithms is to derive invariants between the bits that constitute the variables of a program. Such invariants can often be described with systems of congruences where in each equation c · x = d mod m, m is a power of two, c is a vector of integer coefficients, and x is a vector of propositional variables (bits). Because of the low-level nature of these invariants and the large number of bits that are involved, it is important that the transfer functions can be derived automatically. We address this problem, showing how an analysis for bit-level congruence relationships can be decoupled into two parts: (1) a SAT-based abstraction (compilation) step wh..

View full abstract


Awarded by EPSRC project

Funding Acknowledgements

This work was funded by the EPSRC project EP/F012896, a Royal Society Industrial Fellowship, and a Tewkesbury Fellowship that enabled the first author to visit the University of Melbourne. We thank Tom Reps forhelpful discussions on the notion of a best symbolic transformer.