• English
    • français
  • Help
  •  | 
  • Contact
  •  | 
  • About
  •  | 
  • Login
  • HAL portal
  •  | 
  • Pages Pro
  • EN
  •  / 
  • FR
View Item 
  •   LillOA Home
  • Liste des unités
  • Centre de Recherche en Informatique, Signal et Automatique de Lille (CRIStAL) - UMR 9189
  • View Item
  •   LillOA Home
  • Liste des unités
  • Centre de Recherche en Informatique, Signal et Automatique de Lille (CRIStAL) - UMR 9189
  • View Item
JavaScript is disabled for your browser. Some features of this site may not work without it.

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

Document type :
Communication dans un congrès avec actes
DOI :
10.4204/EPTCS.303.3
Title :
(Co)inductive Proof Systems for Compositional Proofs in Reachability Logic
Author(s) :
Rusu, Vlad [Auteur] refId
Inria Lille - Nord Europe
Nowak, David [Auteur] refId
Extra Small Extra Safe [2XS]
Conference title :
Working Formal Methods Symposium
City :
Timisoara
Country :
Roumanie
Start date of the conference :
2019-09-03
Journal title :
Electronic Proceedings in Theoretical Computer Science (EPTCS)
HAL domain(s) :
Informatique [cs]/Logique en informatique [cs.LO]
English abstract : [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 ...
Show more >
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.Show less >
Language :
Anglais
Peer reviewed article :
Oui
Audience :
Internationale
Popular science :
Non
Collections :
  • Centre de Recherche en Informatique, Signal et Automatique de Lille (CRIStAL) - UMR 9189
Source :
Harvested from HAL
Files
Thumbnail
  • https://hal.inria.fr/hal-02176456v2/document
  • Open access
  • Access the document
Thumbnail
  • https://arxiv.org/pdf/1909.01744
  • Open access
  • Access the document
Thumbnail
  • https://hal.inria.fr/hal-02176456v2/document
  • Open access
  • Access the document
Thumbnail
  • https://hal.inria.fr/hal-02176456v2/document
  • Open access
  • Access the document
Université de Lille

Mentions légales
Université de Lille © 2017