First-order transitive closure axiomatization via iterative invariant injections

Abstract

This paper presents an approach for proving the validity of first-order relational formulas that involve transitive closure. Given a formula F that includes the transitive closure of a relation R, our approach can deduce a complete (pure) first-order axiomatization of the paths of R that occur in F. Such axiomatization enables full automated verification of F using an automatic theorem prover like Z3. This is done via an iterative detection and injection of R-invariants —invariant formulas with respect to R-transitions in the context of F. This paper presents a proof for the correctness of the approach, and reports on its application to non-trivial Alloy benchmarks.