Incorrectness logic for graph programs
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...
Saved in:
| Main Author: | |
|---|---|
| Format: | text |
| Language: | English |
| Published: |
Institutional Knowledge at Singapore Management University
2021
|
| Subjects: | |
| Online Access: | https://ink.library.smu.edu.sg/sis_research/6582 https://ink.library.smu.edu.sg/context/sis_research/article/7585/viewcontent/incorrectness_logic_icgt21.pdf |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| Institution: | Singapore Management University |
| Language: | English |
| 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 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. |
|---|