(Co)inductive proof systems for compositional proofs in reachability logic

DOI10.1016/J.JLAMP.2020.100619MaRDI QIDQ1996855zbMATH OpenOpenAlexWikidataFDO

Authors Vlad Rusu, David Nowak

Publication date 26 February 2021

Published in Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1909.01744

Mathematics Subject Classification ID

Logic in computer science (03B70) Formalization of mathematics in connection with theorem provers (68V20)

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.

Recommendations

• A coinductive approach to proving reachability properties in logically constrained term rewriting systems
• One-path reachability logic
• Soundness and completeness proofs by coinductive methods

Cites work

• A coinductive approach to proving reachability properties in logically constrained term rewriting systems
• A constructor-based reachability logic for rewrite theories
• A generic framework for symbolic execution: a coinductive approach
• An axiomatic basis for computer programming
• Coinduction All the Way Up
• Concurrency verification. Introduction to compositional and noncompositional methods
• Inductive and coinductive components of corecursive functions in Coq
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Introduction to bisimulation and coinduction
• Isabelle/HOL. A proof assistant for higher-order logic
• One-path reachability logic
• Program verification by coinduction
• The power of parameterization in coinductive proof
• Types for proofs and programs. International Workshop TYPES '94, Båstad, Sweden, June 6-10, 1994. Selected papers
• Using Structural Recursion for Corecursion
• Verifying Reachability-Logic Properties on Rewriting-Logic Specifications
• Well-founded recursion with copatterns and sized types

Cited in

(4)

• A coinductive approach to proving reachability properties in logically constrained term rewriting systems
• Soundness and completeness proofs by coinductive methods
• A compositional proof system on a category of labelled transition systems
• scientific article; zbMATH DE number 1223543 (Why is no real title available?)

Describes a project that uses

Uses Software

• Archive of Formal Proofs
• Paco
• Coq
• Isabelle/HOL
• Coinductive

This page was built for publication: (Co)inductive proof systems for compositional proofs in reachability logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1996855)