Anzeige
Erschienen in:
2015 | OriginalPaper | Buchkapitel
First-Order Transitive Closure Axiomatization via Iterative Invariant Injections
verfasst von : Aboubakr Achraf El Ghazi, Mana Taghdiri, Mihai Herda
Erschienen in: NASA Formal Methods
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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.