Skip to Main content Skip to Navigation
Journal articles

Simpler Proofs with Decentralized Invariants

Abstract : When verifying programs where the data have some recursive structure, it is natural to make use of global invariants that are themselves recursively defined. Though this is mathematically elegant, this makes the proofs more complex, as the preservation of these invariants now requires induction. In particular, this makes the proofs less amenable to automation. An alternative is to use local invariants attached to individual components of the structure and which only involve a bounded number of elements. We call these decentralized invariants. When the structure is updated, the footprint of the modification only impacts a limited number of invariants and reestablishing them does not require induction. In this paper, we illustrate this idea on three non-trivial programs, for which we achieve fully automated proofs.
Complete list of metadata

Cited literature [15 references]  Display  Hide  Download

https://hal.inria.fr/hal-02518570
Contributor : Jean-Christophe Filliâtre <>
Submitted on : Wednesday, March 25, 2020 - 12:24:20 PM
Last modification on : Tuesday, April 13, 2021 - 9:36:42 AM
Long-term archiving on: : Friday, June 26, 2020 - 1:37:15 PM

File

main.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-02518570, version 1

Citation

Jean-Christophe Filliâtre. Simpler Proofs with Decentralized Invariants. Journal of Logical and Algebraic Methods in Programming, Elsevier, 2021, 121. ⟨hal-02518570⟩

Share

Metrics

Record views

213

Files downloads

760

Données de recherche

doi: web.