Verifying graph programs with monadic second-order logic

DOI10.1007/978-3-030-78946-6_13MaRDI QIDQ2117269zbMATH OpenOpenAlexFDO

Authors Gia S. Wulandari, Detlef Plump

Publication date 21 March 2022

Full work available at URL https://eprints.whiterose.ac.uk/176053/1/WulandariPlump.ICGT.21.pdf

Mathematics Subject Classification ID

Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Grammars and rewriting systems (68Q42) Specification and verification (program logics, model checking, etc.) (68Q60) Graph theory (including graph drawing) in computer science (68R10)

Recommendations

• Verifying monadic second-order properties of graph programs
• A Hoare calculus for graph programs
• Hoare-style verification of graph programs
• Reasoning about graph programs
• Two-level reasoning about graph transformation programs

Cites work

• Concrete semantics. With Isabelle/HOL
• Correctness of high-level transformation systems relative to nested conditions
• From imperative to rule-based graph programs
• Graph structure and monadic second-order logic. A language-theoretic approach
• Hoare-style verification of graph programs
• scientific article; zbMATH DE number 2016072 (Why is no real title available?)
• scientific article; zbMATH DE number 2110621 (Why is no real title available?)
• scientific article; zbMATH DE number 7456057 (Why is no real title available?)
• The Graph Programming Language GP
• The monadic second-order logic of graphs. I: Recognizable sets of finite graphs
• Verifying monadic second-order properties of graph programs

Cited in

(15)

• Reachability predicates for graph assertions
• Monadic second-order incorrectness logic for GP 2
• Incorrectness logic for graph programs
• Two-level reasoning about graph transformation programs
• Hoare-style verification of graph programs
• A Hoare-like calculus using the \(\mathrm{SROIQ}^{\sigma }\) logic on transformations of graphs
• Verifying monadic second-order properties of graph programs
• A Hoare calculus for graph programs
• Reasoning about graph programs
• Mathematical Foundations of Computer Science 2004
• Towards mechanised proofs in double-pushout graph transformation
• Specification and verification of a linear-time temporal logic for graph transformation
• Mechanised DPO theory: uniqueness of derivations and Church-Rosser theorem
• Formalising the double-pushout approach to graph transformation
• Counterpart-based quantified temporal logics

Describes a project that uses

Uses Software

• Coq
• GP 2

This page was built for publication: Verifying graph programs with monadic second-order logic

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