pith. sign in

arxiv: 1907.05818 · v1 · pith:HFIOQBRFnew · submitted 2019-07-12 · 💻 cs.PL

Verified Self-Explaining Computation

Jan Stolarek , James Cheney This is my paper

Pith reviewed 2026-05-24 22:06 UTC · model grok-4.3

classification 💻 cs.PL
keywords dynamic slicingGalois connectionCoqformal verificationprogram analysisimperative languagedualitydynamic analysis
0
0 comments X

The pith

Forward and backward dynamic slicing form a Galois connection verified in Coq for a simple imperative language.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper formalizes forward and backward dynamic slicing algorithms for a simple imperative language. It proves that these algorithms are dual because they form a Galois connection. The proof of this duality is carried out entirely in the Coq proof assistant. A sympathetic reader would care because the result supplies machine-checked guarantees for a dynamic analysis technique used in debuggers and similar tools.

Core claim

The authors define forward and backward dynamic slicing for an imperative language and establish that the two functions are adjoint, forming a Galois connection; the entire development, including the proof of the connection, is carried out and verified inside Coq.

What carries the argument

The Galois connection between the forward slicing function and the backward slicing function.

If this is right

  • The verified duality supplies a reliable mathematical link between forward and backward slicing results.
  • One slicing direction can be derived from the other via the adjoint property.
  • The Coq development provides a reusable, machine-checked foundation for dynamic program analysis.
  • Slicing-based tools built on this language can inherit the verified duality property.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same adjoint structure may simplify the construction of programs that can explain their own runtime behavior.
  • The verification method could be lifted to richer languages that include procedures or concurrency.
  • Adjoint-based slicing might connect to other program analyses that rely on Galois connections, such as abstract interpretation.
  • Tool builders could extract executable slicing code directly from the verified Coq definitions.

Load-bearing premise

The simple imperative language used in the formalization captures the essential features of slicing that matter for the Galois connection to hold.

What would settle it

A concrete program and input in the formalized language for which forward slicing followed by backward slicing fails to recover the original slice (or the converse) would show the claimed Galois connection does not hold.

Figures

Figures reproduced from arXiv: 1907.05818 by James Cheney, Jan Stolarek.

Figure 1
Figure 1. Figure 1: Input and output lattices and Galois connection corresponding to expression [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Imp syntax 2 Overview 2.1 Imp slicing by example For the purpose of our analysis we use a minimal imperative programming language Imp used in some text￾books on programming languages, e.g. [13, 16, 22]1 . Imp contains arithmetic and logical expressions, mu￾table state (a list of mappings from variable names to numeric values) and a small core of imperative com￾mands: empty instruction (skip), variable assi… view at source ↗
Figure 3
Figure 3. Figure 3: Partial Imp syntax. All elements of syntax from Figure 2 remain unchanged, only [PITH_FULL_IMAGE:figures/full_fig_p004_3.png] view at source ↗
Figure 5
Figure 5. Figure 5: Join operation for arithmetic expressions. [PITH_FULL_IMAGE:figures/full_fig_p005_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: Trace syntax 3. inflation property holds: ∀p∈P p vP g(f(p)) We use this approach in our Coq mechanisation. We will first prove a general theorem that any pair of functions that fulfils properties (1)–(3) above forms a Galois connection. We will then define forward and backward slicing functions for Imp programs and prove that they are monotone, deflationary, and inflationary. Once this is done we will inst… view at source ↗
Figure 7
Figure 7. Figure 7: Imp arithmetic expressions evaluation µ, true ⇒ true :: true µ, false ⇒ false :: false µ, a1 ⇒ T1 :: v1 µ, a2 ⇒ T2 :: v2 µ, a1 = a2 ⇒ T1 = T2 :: v1 =B v2 µ, b ⇒ T :: v µ, ¬b ⇒ ¬T :: ¬Bv µ, b1 ⇒ T1 :: v1 µ, b2 ⇒ T2 :: v2 µ, b1 ∧ b2 ⇒ T1 ∧ T2 :: v1 ∧B v2 [PITH_FULL_IMAGE:figures/full_fig_p006_7.png] view at source ↗
Figure 8
Figure 8. Figure 8: Imp boolean expressions evaluation 6 [PITH_FULL_IMAGE:figures/full_fig_p006_8.png] view at source ↗
Figure 9
Figure 9. Figure 9: Imp command evaluation. T :: µ, % n :: µ, n % n x(va) :: µ, x % µ(x) T1 :: µ, a1 % T1 + T2 :: µ, a1 + a2 % T2 :: µ, a2 % T1 + T2 :: µ, a1 + a2 % T1 :: µ, a1 % v1 T2 :: µ, a2 % v2 T1 + T2 :: µ, a1 + a2 % v1 +N v2 v1, v2 6= [PITH_FULL_IMAGE:figures/full_fig_p007_9.png] view at source ↗
Figure 10
Figure 10. Figure 10: Forward slicing rules for Imp arithmetic expressions. [PITH_FULL_IMAGE:figures/full_fig_p007_10.png] view at source ↗
Figure 11
Figure 11. Figure 11: Forward slicing rules for Imp boolean expressions. [PITH_FULL_IMAGE:figures/full_fig_p008_11.png] view at source ↗
Figure 12
Figure 12. Figure 12: Forward slicing rules for Imp commands. other words, if an arithmetic or logical expression contains at least one hole it will reduce to a ; if it contains no holes it will reduce to a proper value. This is not the case for commands though. For example, command if true then 1 else forward slices to 1, even though it contains a hole in the (not taken) else branch. A rule worth attention is one for forward … view at source ↗
Figure 13
Figure 13. Figure 13: Backward slicing rules for Imp arithmetic expressions. [PITH_FULL_IMAGE:figures/full_fig_p010_13.png] view at source ↗
Figure 14
Figure 14. Figure 14: Backward slicing rules for Imp boolean expressions. [PITH_FULL_IMAGE:figures/full_fig_p010_14.png] view at source ↗
Figure 15
Figure 15. Figure 15: Backward slicing rules for Imp commands. [PITH_FULL_IMAGE:figures/full_fig_p010_15.png] view at source ↗
Figure 16
Figure 16. Figure 16: Slicing a program that computes whether b divides a. (1) r := a(4); (2) whiletrue (b(2) <= r(4)) do { (3) q := q(0) + 1; r := r(4) − b(2) (4) }; (5) whiletrue (b(2) <= r(2)) do { (6) q := q(1) + 1; r := r(2) − b(2) (7) }; (8) whilefalse (b(2) <= r(0)); (9) iffalse (¬(r(0) = 0)) else { (10) res := 1 (11) } [PITH_FULL_IMAGE:figures/full_fig_p012_16.png] view at source ↗
Figure 17
Figure 17. Figure 17: Trace of executing an example program for [PITH_FULL_IMAGE:figures/full_fig_p012_17.png] view at source ↗
read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 2 minor

Summary. The paper formalizes forward and backward dynamic slicing algorithms for a simple imperative programming language and formally verifies (in Coq) that the two algorithms are dual in the sense that they form a Galois connection, thereby confirming a recently proposed mathematical framework for slicing.

Significance. If the result holds, the machine-checked Coq development supplies reusable, formally verified evidence for the Galois-connection duality of dynamic slicing. This is a concrete advance for the verification of dynamic program analyses, an area that has received far less attention than verified compilers or static analyses. The explicit use of an external proof assistant eliminates circularity and provides a reusable artifact.

minor comments (2)
  1. The abstract and introduction would benefit from a single-sentence statement of the main theorem (e.g., “Theorem 3.12 states that …”) so that readers can locate the verified claim immediately.
  2. Notation for the slicing functions and the Galois connection (e.g., the order on slices) should be introduced once in a dedicated “Notation” paragraph rather than piecemeal.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive assessment of the work and their recommendation to accept the paper. We are pleased that the contribution of the machine-checked Coq development for the Galois-connection duality of dynamic slicing is viewed as a concrete advance.

Circularity Check

0 steps flagged

No significant circularity; machine-checked Coq verification is independent

full rationale

The paper defines a simple imperative language, specifies forward and backward dynamic slicing algorithms, and proves they form a Galois connection. This proof is performed and machine-checked inside Coq, which constitutes external verification against the formalized semantics rather than any reduction of the claim to its own fitted inputs or self-citations. No load-bearing step relies on an unverified self-citation chain or renames a result by construction; the Galois connection is established directly by the Coq development for the given model.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The work relies on the standard Coq logic, the definition of the language semantics, and the recently introduced Galois connection framework for slicing.

axioms (1)
  • domain assumption The semantics of the simple imperative language are correctly modeled in Coq.
    The paper relies on defining the language semantics to formalize slicing operations.

pith-pipeline@v0.9.0 · 5608 in / 1062 out tokens · 23975 ms · 2026-05-24T22:06:15.145410+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

22 extracted references · 22 canonical work pages

  1. [1]

    In: Backhouse, R.C., Crole, R.L., Gibbons, J

    Backhouse, R.C.: Galois connections and fixed point calculus. In: Backhouse, R.C., Crole, R.L., Gibbons, J. (eds.) Algebraic and Coalgebraic Methods in the Mathematics of Program Construction, International Summer School and Workshop, Oxford, UK, April 10-14, 2000, Revised Lectures. Lecture Notes in Com- puter Science, vol. 2297, pp. 89–148. Springer (2000...

    work page doi:10.1007/3-540-47797-7 2000

  2. [2]

    Science of Computer Programming 62(3), 228–252 (2006), special issue on Source code analysis and manipulation (SCAM 2005)

    Binkley, D., Danicic, S., Gyim ´othy, T., Harman, M., Kiss, A., Korel, B.: A formalisation of the relationship between forms of program slicing. Science of Computer Programming 62(3), 228–252 (2006), special issue on Source code analysis and manipulation (SCAM 2005)

    work page 2006

  3. [3]

    In: Proceedings of the 2015 Conference on Certified Programs and Proofs

    Blazy, S., Maroneze, A., Pichardie, D.: Verified validation of program slicing. In: Proceedings of the 2015 Conference on Certified Programs and Proofs. pp. 109–117. CPP ’15, ACM, New York, NY, USA (2015)

    work page 2015

  4. [4]

    In: In search of elegance in the theory and practice of computation: a Festschrift in honour of Peter Buneman

    Cheney, J., Acar, U.A., Perera, R.: Toward a theory of self-explaining computation. In: In search of elegance in the theory and practice of computation: a Festschrift in honour of Peter Buneman. pp. 193–216. No. 8000 in LNCS, Springer-Verlag (2013)

    work page 2013

  5. [5]

    Chiang, Y., Mu, S.: Formal derivation of greedy algorithms from relational specifications: A tutorial. J. Log. Algebr. Meth. Program. 85(5), 879–905 (2016). https://doi.org/10.1016/j.jlamp.2015.12.003

    work page doi:10.1016/j.jlamp.2015.12.003 2016

  6. [6]

    Cambridge University Press (2002)

    Davey, B.A., Priestley, H.A.: Introduction to Lattices and Order. Cambridge University Press (2002)

    work page 2002

  7. [7]

    In: Mathematics of Program Construction, 8th Inter- national Conference, MPC 2006, Kuressaare, Estonia, July 3-5, 2006, Proceedings

    Gibbons, J.: Fission for program comprehension. In: Mathematics of Program Construction, 8th Inter- national Conference, MPC 2006, Kuressaare, Estonia, July 3-5, 2006, Proceedings. pp. 162–179 (2006). https://doi.org/10.1007/11783596 12

    work page doi:10.1007/11783596 2006

  8. [8]

    Information Processing Letters 29(3), 155–163 (1988)

    Korel, B., Laski, J.: Dynamic program slicing. Information Processing Letters 29(3), 155–163 (1988)

    work page 1988

  9. [9]

    Formal Aspects of Computing 30(1), 107–131 (Jan 2018)

    L ´echenet, J., Kosmatov, N., Gall, P .L.: Cut branches before looking for bugs: certifiably sound verification on relaxed slices. Formal Aspects of Computing 30(1), 107–131 (Jan 2018)

    work page 2018

  10. [10]

    In: ERTS 2016: Embedded Real Time Software and Systems

    Leroy, X., Blazy, S., K ¨astner, D., Schommer, B., Pister, M., Ferdinand, C.: Compcert – a formally verified optimizing compiler. In: ERTS 2016: Embedded Real Time Software and Systems. SEE (2016)

    work page 2016

  11. [11]

    Mu, S., Ko, H., Jansson, P .: Algebra of programming in Agda: Dependent types for relational program derivation. J. Funct. Program. 19(5), 545–579 (2009). https://doi.org/10.1017/S0956796809007345

    work page doi:10.1017/s0956796809007345 2009

  12. [12]

    Mu, S., Oliveira, J.N.: Programming from Galois connections. J. Log. Algebr. Program. 81(6), 680–704 (2012). https://doi.org/10.1016/j.jlap.2012.05.003

    work page doi:10.1016/j.jlap.2012.05.003 2012

  13. [13]

    Springer-Verlag, Berlin, Heidelberg (1999) 17

    Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis. Springer-Verlag, Berlin, Heidelberg (1999) 17

    work page 1999

  14. [14]

    In: CONCUR

    Perera, R., Garg, D., Cheney, J.: Causally consistent dynamic slicing. In: CONCUR. pp. 18:1–18:15 (2016)

    work page 2016

  15. [15]

    In: ICFP

    Perera, R., Acar, U.A., Cheney, J., Levy, P .B.: Functional programs that explain their work. In: ICFP . pp. 365–376. ACM (2012)

    work page 2012

  16. [16]

    Electronic textbook (2017), version 5.0

    Pierce, B.C., de Amorim, A.A., Casinghino, C., Gaboardi, M., Greenberg, M., Hrit ¸cu, C., Sj ¨oberg, V ., Yorgey, B.: Software Foundations. Electronic textbook (2017), version 5.0. http://www.cis.upenn. edu/˜bcpierce/sf

    work page 2017

  17. [17]

    Proceedings of the ACM on Programming Languages (PACMPL)1(ICFP) (Sep 2017)

    Ricciotti, W., Stolarek, J., Perera, R., Cheney, J.: Imperative functional programs that explain their work. Proceedings of the ACM on Programming Languages (PACMPL)1(ICFP) (Sep 2017)

    work page 2017

  18. [18]

    Silva, J.: An analysis of the current program slicing and algorithmic debugging based techniques. Tech. rep., Technical University of Valencia (2008)

    work page 2008

  19. [19]

    Stolarek, J.: Verified self-explaining computation (May 2019), https://bitbucket.org/jstolarek/ gc_imp_slicing/src/mpc_2019_submission/

    work page 2019

  20. [20]

    https://doi.org/10.5281/zenodo.1028037

    The Coq Development Team: The Coq proof assistant, version 8.7.0 (Oct 2017). https://doi.org/10.5281/zenodo.1028037

    work page doi:10.5281/zenodo.1028037 2017

  21. [21]

    In: ICSE

    Weiser, M.: Program slicing. In: ICSE. pp. 439–449. IEEE Press, Piscataway, NJ, USA (1981)

    work page 1981

  22. [22]

    MIT Press, Cambridge, MA, USA (1993) 18

    Winskel, G.: The Formal Semantics of Programming Languages: An Introduction. MIT Press, Cambridge, MA, USA (1993) 18

    work page 1993