# Verified Self-Explaining Computation

## TL;DR

This paper introduces a formal framework for verifying dynamic program slicing algorithms, demonstrating their duality through proof assistant verification, advancing the reliability of program analysis tools.

## Contribution

It formalizes and verifies the duality of forward and backward dynamic slicing algorithms within a simple imperative language using Coq.

## Key findings

- Formal proof of duality between slicing algorithms
- Verification of slicing algorithms in Coq
- Enhanced understanding of dynamic analysis correctness

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