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

Rusu, Vlad; Nowak, David

Type de document :

Communication dans un congrès avec actes

DOI :

10.4204/EPTCS.303.3

Titre :

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

Auteur(s) :

Rusu, Vlad [Auteur]
Centre Inria de l'Université de Lille
Nowak, David [Auteur]

Extra Small Extra Safe [2XS]

Titre de la manifestation scientifique :

Working Formal Methods Symposium

Ville :

Timisoara

Pays :

Roumanie

Date de début de la manifestation scientifique :

2019-09-03

Titre de la revue :

Electronic Proceedings in Theoretical Computer Science (EPTCS)

Discipline(s) HAL :

Informatique [cs]/Logique en informatique [cs.LO]

Résumé en anglais : [en]

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 ...
Lire la suite >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.Lire moins >

Langue :

Anglais

Comité de lecture :

Oui

Audience :

Internationale

Vulgarisation :

Non

Collections :

Centre de Recherche en Informatique, Signal et Automatique de Lille (CRIStAL) - UMR 9189

Source :

Harvested from HAL

Fichiers

https://hal.inria.fr/hal-02176456v2/document
Accès libre
Accéder au document

https://arxiv.org/pdf/1909.01744
Accès libre
Accéder au document

https://hal.inria.fr/hal-02176456v2/document
Accès libre
Accéder au document

https://hal.inria.fr/hal-02176456v2/document
Accès libre
Accéder au document

document
Accès libre
Accéder au document

from2019_full.pdf
Accès libre
Accéder au document

1909.01744
Accès libre
Accéder au document

(Co)inductive Proof Systems for Compositional ... BibTeX CSV Excel RIS

Fichiers

(Co)inductive Proof Systems for Compositional ...

BibTeX

CSV

Excel

RIS