Approximating the Transitive Closure of a Boolean-Affine Relation
Paul Feautrier, Ens De Lyon · 2012
Boolean affine relations, which combine affine inequalities by boolean connectives are ubiquitous in all kind of static program analyzes. One of the crucial operations on such relations is transitive closure, which is closely related to the construction of loop inductive invariants. I present here a new over-approximation algorithm, which has the interest-ing property of being extendible for increased precision.