Publication Type

Conference Proceeding Article

Version

acceptedVersion

Publication Date

6-2021

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 a nondeterministic graph programming language, and show how it can be used to reason deductively about program incorrectness, whether defined by the presence of forbidden graph structure or by finitely failing executions. We prove this 'incorrectness logic' to be sound and complete, and speculate on some possible future applications of it.

Keywords

Program logics, under-approximate reasoning, bugs

Discipline

Programming Languages and Compilers | Software Engineering

Research Areas

Software and Cyber-Physical Systems

Publication

Proceedings of the 14th International Conference on Graph Transformation (ICGT 2021), Bergen Norway, June 24-25

Volume

12741

First Page

81

Last Page

101

Identifier

10.1007/978-3-030-78946-6_5

Publisher

Springer

City or Country

Cham

Download

Share

COinS