A Hoare calculus for graph programs

DOI10.1007/978-3-642-15928-2_10MaRDI QIDQ4931309zbMATH OpenOpenAlexFDO

Authors Christopher M. Poskitt, Detlef Plump

Publication date 4 October 2010

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://ink.library.smu.edu.sg/sis_research/4918

Mathematics Subject Classification ID

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

Recommendations

• Hoare-style verification of graph programs
• Verifying graph programs with monadic second-order logic
• Verifying monadic second-order properties of graph programs
• A Hoare-like calculus using the \(\mathrm{SROIQ}^{\sigma }\) logic on transformations of graphs
• Reasoning about graph programs

Cited in

(11)

• Monadic second-order incorrectness logic for GP 2
• Verifying graph programs with monadic second-order logic
• Hoare-style verification of graph programs
• Ensuring correctness of model transformations while remaining decidable
• A Hoare-like calculus using the \(\mathrm{SROIQ}^{\sigma }\) logic on transformations of graphs
• Verifying monadic second-order properties of graph programs
• Reasoning about graph programs
• scientific article; zbMATH DE number 7456057 (Why is no real title available?)
• Graph Transformations
• Proving correctness of logically decorated graph rewriting systems
• A strict constrained superposition calculus for graphs

Describes a project that uses

Uses Software

• GrGen

This page was built for publication: A Hoare calculus for graph programs

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