Skip to Main content Skip to Navigation
Conference papers

(Co)inductive Proof Systems for Compositional Proofs in Reachability Logic

Vlad Rusu 1 David Nowak 2
2 2XS - Extra Small Extra Safe
CRIStAL - Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189
Abstract : Reachability Logic is a formalism that can be used, among others, for expressing partial-correctness properties of transition systems. In this paper we present three proof systems for this formalism, all of which are sound and complete and inherit the coinductive nature of the logic. The proof systems differ, however, in several aspects. First, they use induction and coinduction in different proportions. The second aspect regards compositionality, broadly meaning their ability to prove simpler formulas on smaller systems, and to reuse those formulas as lemmas for more complex formulas on larger systems. The third aspect is the difficulty of their soundness proofs. We show that the more induction a proof system uses, and the more specialised is its use of coinduction (with respect to our problem domain), the more compositional the proof system is, but the more difficult its soundness proof becomes. We also briefly present mechanisations of these results in the Isabelle/HOL and Coq proof assistants.
Document type :
Conference papers
Complete list of metadata

Cited literature [61 references]  Display  Hide  Download

https://hal.inria.fr/hal-02176456
Contributor : Pal Dream <>
Submitted on : Friday, August 23, 2019 - 10:32:38 AM
Last modification on : Friday, December 11, 2020 - 6:44:03 PM

File

from2019_full.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Vlad Rusu, David Nowak. (Co)inductive Proof Systems for Compositional Proofs in Reachability Logic. Working Formal Methods Symposium, Sep 2019, Timisoara, Romania. pp. 32-47, ⟨10.4204/EPTCS.303.3⟩. ⟨hal-02176456v2⟩

Share

Metrics

Record views

102

Files downloads

571