Incorrectness logic for graph programs
From MaRDI portal
Publication:2117260
DOI10.1007/978-3-030-78946-6_5zbMATH Open1492.68041arXiv2105.04501OpenAlexW3174501452MaRDI QIDQ2117260FDOQ2117260
Publication date: 21 March 2022
Abstract: Program logics typically reason about an over-approximation of program behaviour to prove the absence of bugs. Recently, program logics have been proposed that instead prove the presence of bugs by means of under-approximate reasoning, which has the promise of better scalability. In this paper, we present an under-approximate program logic for a nondeterministic graph programming language, and show how it can be used to reason deductively about program incorrectness, whether defined by the presence of forbidden graph structure or by finitely failing executions. We prove this incorrectness logic to be sound and complete, and speculate on some possible future applications of it.
Full work available at URL: https://arxiv.org/abs/2105.04501
Recommendations
- Reasoning about graph programs
- scientific article; zbMATH DE number 7456057
- Proving correctness of logically decorated graph rewriting systems
- Hoare-style verification of graph programs
- Proving correctness of compilers using structured graphs
- Graph theoretical structures in logic programs and default theories
- Verification of graph grammars using a logical approach
- Verifying graph programs with monadic second-order logic
Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Logic in computer science (03B70)
Cites Work
- An axiomatic basis for computer programming
- Soundness and Completeness of an Axiom System for Program Verification
- Verifying Monadic Second-Order Properties of Graph Programs
- Correctness of high-level transformation systems relative to nested conditions
- Verification of Graph Transformation Systems with Context-Free Specifications
- Verification of sequential and concurrent programs
- A framework for the verification of infinite-state graph transformation systems
- Hoare-style verification of graph programs
- Institutions for navigational logics for graphical structures
- Formal Verification of Invariants for Attributed Graph Transformation Systems Based on Nested Attributed Graph Conditions
- Weakest Preconditions for High-Level Programs
- Verifying graph transformation systems with description logics
- Title not available (Why is that?)
- A navigational logic for reasoning about graph properties
- Reverse Hoare Logic
- Local reasoning about the presence of bugs: incorrectness separation logic
- Two-level reasoning about graph transformation programs
- Title not available (Why is that?)
Cited In (2)
Uses Software
This page was built for publication: Incorrectness logic for graph programs
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2117260)
