Incorrectness logic for graph programs

DOI10.1007/978-3-030-78946-6_5MaRDI QIDQ2117260zbMATH OpenOpenAlexFDO

Authors Christopher M. Poskitt

Publication date 21 March 2022

Full work available at URL https://arxiv.org/abs/2105.04501, https://ink.library.smu.edu.sg/sis_research/6582

zbMATH Keywords

program logicsunder-approximate reasoningbugs

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Logic in computer science (03B70)

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.

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

Cites work

• scientific article; zbMATH DE number 2016072 (Why is no real title available?)
• scientific article; zbMATH DE number 7456057 (Why is no real title available?)
• A framework for the verification of infinite-state graph transformation systems
• A navigational logic for reasoning about graph properties
• An axiomatic basis for computer programming
• Correctness of high-level transformation systems relative to nested conditions
• Formal verification of invariants for attributed graph transformation systems based on nested attributed graph conditions
• Hoare-style verification of graph programs
• Institutions for navigational logics for graphical structures
• Local reasoning about the presence of bugs: incorrectness separation logic
• Reverse Hoare logic
• Soundness and Completeness of an Axiom System for Program Verification
• Two-level reasoning about graph transformation programs
• Verification of graph transformation systems with context-free specifications
• Verification of sequential and concurrent programs
• Verifying graph transformation systems with description logics
• Verifying monadic second-order properties of graph programs
• Weakest Preconditions for High-Level Programs

Cited in

(3)

• Limits and difficulties in the design of under-approximation abstract domains
• Local completeness logic on Kleene algebra with tests
• Monadic second-order incorrectness logic for GP 2

Describes a project that uses

Uses Software

• SEET
• GROOVE

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)