Automated Software Analysis Group

TCProver: A Prover for the FOL+TC Fragment

TCProver is a full automatic tool for proving valid formulas of the fragment of first-order logic enriched with (finite) relations and transitive closure (TC). TCProver focuses in its current version on Alloy -- a declarative first-order relational logic with built-in operators for transitive closure and cardinality.

TCProver uses an approach based on a basic non complete first-order axiomatization of TC together with an algorithm for detecting and injecting so-called R-Path invariants. 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.





We will be happy to share the tool upon your request. Please feel free to send an email to A. Achraf El Ghazi or Mana Taghdiri.