Monadic second-order incorrectness logic for GP 2
From MaRDI portal
Publication:2096431
DOI10.1016/j.jlamp.2022.100825OpenAlexW4298127348MaRDI QIDQ2096431
Detlef Plump, Christopher M. Poskitt
Publication date: 16 November 2022
Published in: Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.jlamp.2022.100825
monadic second-order logiccorrectness proofsgraph transformationprogram logicsunder-approximate reasoning
Related Items (1)
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Verification of sequential and concurrent programs
- A framework for the verification of infinite-state graph transformation systems
- Verifying graph transformation systems with description logics
- Towards a navigational logic for graphical structures
- A structural approach to operational semantics
- A navigational logic for reasoning about graph properties
- Incorrectness logic for graph programs
- Verifying graph programs with monadic second-order logic
- Local reasoning about the presence of bugs: incorrectness separation logic
- Two-level reasoning about graph transformation programs
- Double-pushout graph transformation revisited
- Hoare-Style Verification of Graph Programs
- $\mathcal M, \mathcal N$ -Adhesive Transformation Systems
- Reverse Hoare Logic
- Verifying Monadic Second-Order Properties of Graph Programs
- Weakest Preconditions for High-Level Programs
- Correctness of high-level transformation systems relative to nested conditions
- Soundness and Completeness of an Axiom System for Program Verification
- Interactive and automated proofs for graph transformations
- Verification of Graph Transformation Systems with Context-Free Specifications
- Formal Verification of Invariants for Attributed Graph Transformation Systems Based on Nested Attributed Graph Conditions
- Symbolic Model Generation for Graph Properties
- An axiomatic basis for computer programming
This page was built for publication: Monadic second-order incorrectness logic for GP 2
