Incorrectness logic for graph programs

DOI10.1007/978-3-030-78946-6_5zbMath1492.68041arXiv2105.04501OpenAlexW3174501452MaRDI QIDQ2117260

Christopher M. Poskitt

Publication date: 21 March 2022

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

zbMATH Keywords

program logicsunder-approximate reasoningbugs

Mathematics Subject Classification ID

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

Related Items (2)

Local completeness logic on Kleene algebra with tests ⋮ Monadic second-order incorrectness logic for GP 2

Uses Software

• GROOVE
• SEET

Cites Work

• Unnamed Item
• Unnamed Item
• Institutions for navigational logics for graphical structures
• Verification of sequential and concurrent programs
• A framework for the verification of infinite-state graph transformation systems
• Verifying graph transformation systems with description logics
• A navigational logic for reasoning about graph properties
• Local reasoning about the presence of bugs: incorrectness separation logic
• Two-level reasoning about graph transformation programs
• Hoare-Style Verification of Graph Programs
• 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
• Verification of Graph Transformation Systems with Context-Free Specifications
• Formal Verification of Invariants for Attributed Graph Transformation Systems Based on Nested Attributed Graph Conditions
• An axiomatic basis for computer programming

This page was built for publication: Incorrectness logic for graph programs