Computer Sciences Dept.

Abstract Domains of Affine Relations

Matt Elder, Junghee Lim, Tushar Sharma, Tycho Andersen,Thomas Reps

This paper considers some known abstract domains for affine-relation analysis (ARA), along with several variants, and studies how they relate to each other. We show that the abstract domains of Mueller-Olm/Seidl (MOS) and King/Sondergaard (KS) are, in general, incomparable, but give sound interconversion methods. We also show that the methods of King and Sondergaard can be applied without bit-blasting -- while still using a bit-precise concrete semantics.

Download this report (PDF)

Return to tech report index

Computer Science | UW Home