© University of Kent - Contact | Feedback | Legal | FOI | Cookies
Automatic Abstraction for Congruences
Andy King and Harald Sondergaard
In Gilles Barthe and Manuel Hermenegildo, editors, Eleventh International Conference on Verification, Model Checking, and Abstract Interpretation, number 5944 in Lecture Notes in Computer Science, pages 182-196. Springer-Verlag, January 2010.Abstract
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 $\vec{c} \cdot \vec{x} = d \mod m$, (unknown variable m)$ is a power of two, $\vec{c}$ is a vector of integer coefficients, and $\vec{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 which can be automated, and (2) an interpretation step that requires no SAT-solving. We exploit triangular matrix forms to derive transfer functions efficiently, even in the presence of large numbers of bits. Finally we propose program transformations that improve the analysis results.
Download publication 209 kbytes (PDF)Bibtex Record
@inproceedings{2966,
author = {Andy King and Harald S{o}ndergaard},
title = {Automatic {A}bstraction for {C}ongruences},
month = {January},
year = {2010},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/2010/2966},
publication_type = {inproceedings},
submission_id = {19766_1258980473},
booktitle = {Eleventh International Conference on Verification, Model Checking, and Abstract Interpretation},
editor = {Gilles Barthe and Manuel Hermenegildo},
number = {5944},
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag},
refereed = {yes},
}