Automatic Abstraction for Congruences

King, Andy and Sondergaard, Harald (2010) Automatic Abstraction for Congruences. In: Barthe, Gilles and Hermenegildo, Manuel, eds. Verification, Model Checking, and Abstract Interpretation. Lecture Notes in Computer Science (5944). Springer-Verlag, pp. 182-196. ISBN 978-3-642-11318-5. (Full text available)

PDF
Download (214kB) Preview
[img]
Preview
Official URL
http://www.cs.kent.ac.uk/pubs/2010/2966

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.

Item Type: Book section
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Faculties > Science Technology and Medical Studies > School of Computing > Programming Languages and Systems Group
Faculties > Science Technology and Medical Studies > School of Computing > Security Group
Depositing User: Andy King
Date Deposited: 21 Sep 2012 09:49
Last Modified: 12 Dec 2013 12:54
Resource URI: http://kar.kent.ac.uk/id/eprint/30704 (The current URI for this page, for reference purposes)
  • Depositors only (login required):

Downloads

Downloads per month over past year