Monadic second-order incorrectness logic for GP 2

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 p...

Full description

Saved in:
Bibliographic Details
Main Authors: POSKITT, Christopher M., PLUMP, Detlef
Format: text
Language:English
Published: Institutional Knowledge at Singapore Management University 2023
Subjects:
Online Access:https://ink.library.smu.edu.sg/sis_research/7335
https://ink.library.smu.edu.sg/context/sis_research/article/8338/viewcontent/mso_incorrectness_logic_jlamp23.pdf
Tags: Add Tag
No Tags, Be the first to tag this record!
Institution: Singapore Management University
Language: English
Description
Summary: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.