Verified Self-Explaining Computation

Jan Stolarek, James Cheney

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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 formalizes forward and backward dynamic slicing algorithms for a simple imperative programming language, and formally verifies their duality using the Coq proof assistant.
Original languageEnglish
Title of host publicationMathematics of Program Construction
Subtitle of host publication13th International Conference, MPC 2019, Porto, Portugal, October 7-9, 2019. Proceedings
EditorsGraham Hutton
PublisherSpringer
Pages76-102
Number of pages27
ISBN (Electronic)978-3-030-33636-3
ISBN (Print)978-3-030-33635-6
DOIs
Publication statusPublished - 20 Oct 2019
Event13th International Conference on Mathematics of Program Construction - Porto, Portugal
Duration: 7 Oct 20199 Oct 2019
http://www.cs.nott.ac.uk/~pszgmh/mpc19.html

Publication series

NameLecture Notes in Computer Science
PublisherSpringer International Publishing
Volume11825
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference13th International Conference on Mathematics of Program Construction
Abbreviated titleMPC 2019
Country/TerritoryPortugal
CityPorto
Period7/10/199/10/19
Internet address

Fingerprint

Dive into the research topics of 'Verified Self-Explaining Computation'. Together they form a unique fingerprint.

Cite this