Automated Software Analysis Group

First-Order Transitive Closure Axiomatization via Iterative Invariant Injections

  • Author:

    Aboubakr Achraf El Ghazi, Mana Taghdiri, Mihai Herda

  • Place:

    7th NASA Formal Methods Symposium (NFM), Pasadena,  April  2015

  • 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.


    author     = {Aboubakr Achraf {El Ghazi} and Mana Taghdiri and Mihai Herda},
    title         = {First-Order Transitive Closure Axiomatization via Iterative Invariant Injections},
    booktitle  = {7th NASA Formal Methods Symposium (NFM)},
    pages      = {143-157},
    address   = {Pasadena},
    year        = {2015},
    month     = {April}