Executable Transitive Closures

We provide a generic work-list algorithm to compute the (reflexi-ve-)transitive closure of relations where only successors of newly de-tected states are generated. In contrast to our previous work [2], the relations do not have to be finite, but each element must only have finitely many (indirect) successors. Moreover, a subsumption relation can be used instead of pure equality. An executable variant of the al-gorithm is available where the generic operations are instantiated with list operations. This formalization was performed as part of the IsaFoR/CeTA project1 [3], and it has been used to certify size-change termination proofs where large transitive closures have to be computed. Contents 1 A work-list algorithm for reflexive-transitive closures 1 1.1 The generic case.........................