Verified Self-Explaining Computation
Programming Languages
2019-07-15 v1
Abstract
Common programming tools, like compilers, debuggers, and IDEs, crucially rely on the ability to analyse program code to reason about its behaviour and properties. There has been a great deal of work on verifying compilers and static analyses, but far less on verifying dynamic analyses such as program slicing. Recently, a new mathematical framework for slicing was introduced in which forward and backward slicing are dual in the sense that they constitute a Galois connection. This paper formalises forward and backward dynamic slicing algorithms for a simple imperative programming language, and formally verifies their duality using the Coq proof assistant.
Cite
@article{arxiv.1907.05818,
title = {Verified Self-Explaining Computation},
author = {Jan Stolarek and James Cheney},
journal= {arXiv preprint arXiv:1907.05818},
year = {2019}
}