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.

links

BibTex

@InProceedings{a.a.elghazi-nfm2015,
    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}
}