King, Andy and Sondergaard, Harald (2010) Automatic Abstraction for Congruences. In: Barthe, Gilles and Hermenegildo, Manuel V., eds. Verification, Model Checking, and Abstract Interpretation. Lecture Notes in Computer Science (5944). SpringerVerlag, pp. 182196. ISBN 9783642113185. (KAR id:30704)
PDF
Language: English 

Download this file (PDF/240kB) 
Preview 
Request a format suitable for use with assistive technology e.g. a screenreader  
Official URL: http://www.cs.kent.ac.uk/pubs/2010/2966 
Abstract
One approach to verifying bittwiddling 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 lowlevel 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 bitlevel congruence relationships can be decoupled into two parts: (1) a SATbased abstraction (compilation) step which can be automated, and (2) an interpretation step that requires no SATsolving. 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:  Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing 
Depositing User:  Andy King 
Date Deposited:  21 Sep 2012 09:49 UTC 
Last Modified:  16 Nov 2021 10:08 UTC 
Resource URI:  https://kar.kent.ac.uk/id/eprint/30704 (The current URI for this page, for reference purposes) 
 Link to SensusAccess
 Export to:
 RefWorks
 EPrints3 XML
 BibTeX
 CSV
 Depositors only (login required):