We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:

Download:

Current browse context:

cs.LO

Change to browse by:

cs

References & Citations

DBLP - CS Bibliography

Bookmark

(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo ScienceWISE logo

Computer Science > Logic in Computer Science

Title: Incorrectness Logic for Graph Programs

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.
Comments: Accepted by the 14th International Conference on Graph Transformation (ICGT 2021)
Subjects: Logic in Computer Science (cs.LO)
Journal reference: Proc. ICGT 2021, volume 12741 of LNCS, pages 81-101. Springer, 2021
DOI: 10.1007/978-3-030-78946-6_5
Cite as: arXiv:2105.04501 [cs.LO]
  (or arXiv:2105.04501v2 [cs.LO] for this version)

Submission history

From: Christopher M. Poskitt [view email]
[v1] Mon, 10 May 2021 16:50:35 GMT (3747kb,D)
[v2] Thu, 13 May 2021 06:09:41 GMT (3746kb,D)

Link back to: arXiv, form interface, contact.