Publication Type

Journal Article

Version

submittedVersion

Publication Date

1-2023

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 GP 2, a rule-based programming language for manipulating graphs. We define the proof rules of this program logic extensionally, i.e. independently of fixed assertion languages, then instantiate them with a morphism-based assertion language able to specify monadic second-order properties on graphs (e.g. path properties). We show how these proof rules can be used to reason deductively about the presence of forbidden graph structure or failing executions. Finally, we prove our 'incorrectness logic' to be sound, and our extensional proof rules to be relatively complete.

Keywords

Program logics, correctness proofs, under-approximate reasoning, monadic second-order logic, graph transformation

Discipline

Software Engineering

Research Areas

Software and Cyber-Physical Systems

Publication

Journal of Logical and Algebraic Methods in Programming

Volume

130

First Page

1

Last Page

30

ISSN

2352-2208

Identifier

10.1016/j.jlamp.2022.100825

Publisher

Elsevier

Embargo Period

1-1-2025

Additional URL

http://doi.org/10.1016/j.jlamp.2022.100825

Download

Available for download on Wednesday, January 01, 2025

Share

COinS