Projects per year
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 language | English |
---|---|
Title of host publication | Mathematics of Program Construction |
Subtitle of host publication | 13th International Conference, MPC 2019, Porto, Portugal, October 7-9, 2019. Proceedings |
Editors | Graham Hutton |
Publisher | Springer |
Pages | 76-102 |
Number of pages | 27 |
ISBN (Electronic) | 978-3-030-33636-3 |
ISBN (Print) | 978-3-030-33635-6 |
DOIs | |
Publication status | Published - 20 Oct 2019 |
Event | 13th International Conference on Mathematics of Program Construction - Porto, Portugal Duration: 7 Oct 2019 → 9 Oct 2019 http://www.cs.nott.ac.uk/~pszgmh/mpc19.html |
Publication series
Name | Lecture Notes in Computer Science |
---|---|
Publisher | Springer International Publishing |
Volume | 11825 |
ISSN (Print) | 0302-9743 |
ISSN (Electronic) | 1611-3349 |
Conference
Conference | 13th International Conference on Mathematics of Program Construction |
---|---|
Abbreviated title | MPC 2019 |
Country/Territory | Portugal |
City | Porto |
Period | 7/10/19 → 9/10/19 |
Internet address |
Fingerprint
Dive into the research topics of 'Verified Self-Explaining Computation'. Together they form a unique fingerprint.Projects
- 2 Finished
-
-
Skye-A programming language bridging theory and practice for scientific data curation
1/09/16 → 28/02/23
Project: Research