Pith. sign in

REVIEW 3 major objections 4 minor 52 references

CF-GKAT: Efficient Validation of Control-Flow Transformations

T0 review · 3 major / 4 minor · reviewed 2026-08-12 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read CF-GKAT decides trace equivalence of programs with goto, break, and return soundly and completely in nearly-linear time.

desk verdict Solid, Coq-verified theory; the printed lowering definition has a typo that makes it ill-typed, but the underlying result looks right and deserves a referee. read the letter →

arxiv 2411.13220 v2 pith:PW534WKG submitted 2024-11-20 cs.PL

Cheng Zhang , Tobias Kappé , David E. Narváez , Nico Naus This is my paper · ORCID
classification cs.PL MSC 68Q6068Q4503B70
keywords control-flowequivalenceguardedKleenealgebrawithtestsindicatorvariablesnon-localcontrolflowtracegotoeliminationdecompilervalidationcontinuationsemantics
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

CF-GKAT extends guarded Kleene algebra with tests (GKAT) — an algebraic framework that equates programs whenever the same test outcomes always lead to the same sequence of uninterpreted actions — with two capabilities GKAT lacked: indicator variables, a single value programs can set and test, and non-local control flow (goto, break, return). The paper aims to make automatic trace-equivalence checking usable for real control-flow transformations, such as goto-elimination, decompiler loop structuring, and rewrites into single Böhm-Jacopini loops, where the interesting question is whether two very differently written programs always take the same action path. Its central claim is that trace equivalence of CF-GKAT programs is decidable soundly and completely by reducing it to GKAT automaton bisimulation, with cost roughly $|I|^2 \times (|e|+|f|)$ — nearly linear in program size when the test alphabet is fixed. To back the claim, the paper's checker validates the output of a goto-elimination tool and of the Ghidra decompiler on a function from GNU Coreutils. A sympathetic reader should care because this offers a fast, automatic way to certify that control-flow-manipulating tools preserve observable behavior.

What carries the argument

The argument is carried by two intermediate objects. The first is the continuation, a tag attached to each guarded word that records how control proceeds after that trace ends: $\mathrm{acc}_i$ (normal termination with indicator value $i$), $\mathrm{brk}_i$ (break out of the enclosing loop), $\mathrm{ret}$ (return from the whole program), or $\mathrm{jmp}(\ell,i)$ (continue at label $\ell$). Tagging traces this way lets the otherwise non-compositional constructs goto, break, and return get an inductive semantics, with jump resolution deferred until the whole program is known. The second is the CF-GKAT automaton: a transition function of type $I \times \mathrm{At} \to \bot + C + \Sigma{\times}S{\times}I$ together with a jump map assigning a transition to every label. Expressions compile to these automata by a Thompson-style construction whose iterated start dynamics handles the subtle case where a loop body changes the indicator value without executing any action. Lowering to GKAT automata is the reduction that does the work: indicator values become part of the state, jumps are resolved by iterating the jump map (cycles become rejection), break continuations become rejection, and return becomes acceptance — after which the existing GKAT bisimulation check decides the question.

What would settle it

Compute, by the explicit definitions in the paper, the trace language of the goto-based program and of the break-based loop from the introduction over one test and a two-valued indicator set: this is a finite enumeration of guarded words, and any guarded word present in one language but not the other would refute the claim that CF-GKAT equates the two. A sharper boundary test targets completeness: the algorithm assumes that starting indicator values absent from both programs all behave alike, so any expression whose traces depend on which absent value it starts from would produce a false equivalence verdict.

Watch

Extended reading notes

Core claim

The paper's central claim is that the procedure equivCFGKAT decides trace equivalence exactly: for CF-GKAT programs $e$ and $f$ it returns true precisely when the two programs have the same guarded-language semantics — for every initial truth assignment to the primitive tests and every starting indicator value, they execute the same sequence of uninterpreted actions in the same order. The procedure converts each program into a CF-GKAT automaton by a Thompson-style construction that preserves an intermediate continuation semantics, lowers each automaton to a GKAT automaton by embedding indicator values into the state space and resolving jump continuations through the label map, and runs the existing GKAT bisimulation check for every starting indicator value (including one fresh value not appearing in either program). Soundness and completeness follow from two theorems — the Thompson construction preserves the continuation semantics, and lowering commutes with semantic jump resolution — both backed by a machine-checked formalization; the equivalence checks cost on the order of $|I|^2 \times (|e|+|f|)$ and automaton construction about $|L|\times|I| + |I|\times(|e|+|f|)$, so the method inherits GKAT's near-linear complexity.

Load-bearing premise

Everything rests on the premise that the indicator variable never appears in any primitive test or action, so it is purely a control-flow value — if the program's key variable is read or written by other operations, CF-GKAT's semantics no longer describes the program and the checker's verdict is meaningless for it.

Editorial extensions

If this is right

  • Decompiler and refactoring tooling gains an automatic oracle for control-flow-preserving rewrites: the paper's checker validates both a goto-elimination pass and Ghidra's control-flow structuring of a compiled GNU Coreutils function, each in under a second.
  • The decidable class extends from while-programs to programs with goto, break, return, and assignments of hardcoded values to an isolated variable — covering pseudo-assembly input, decompiled code, and single-loop normal forms from the Böhm-Jacopini construction.
  • Trace-equivalence checking keeps GKAT's efficiency: with the test alphabet fixed, the algorithm is nearly linear in the sizes of the two programs and linear in the number of labels, with cost quadratic only in the number of indicator values.
  • The automaton construction answers an open question in the Kleene-algebra literature about whether non-local control flow can be handled directly, by compiling expressions to automata rather than first encoding gotos away.
  • Because the final indicator value is invisible in the trace semantics, CF-GKAT equates programs that differ only in their final indicator value, and the resulting equivalence is not a congruence: programs must be compared as wholes, not in arbitrary contexts.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • The framework's natural sweet spot is compiler-generated control flow, where a 'mode' or 'state' variable is written only by dispatcher assignments and read only by dispatcher tests; a testable extension is to measure how many functions in a large C corpus admit such an isolated variable without rewriting.
  • The construction extends in a straightforward way to several indicator variables, since the semantics is indexed by the indicator set; the cost would multiply by the product of the value sets, which would cover structuring passes that introduce more than one state variable.
  • A consequence the paper leaves implicit is that an infinite loop that only cycles through indicator values is identified with outright rejection, since the jump-resolution fixed point returns $\bot$ on cycles; users who care about termination-sensitive transformations should notice this identification.
  • The practical bottleneck is the front-end: choosing which C variable is the indicator and normalizing decompiler artifacts (value masking, temporary-assignment propagation) were done by hand in the case study, and automating those steps is what would determine how broadly the method applies.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 4 minor

Summary. The paper introduces CF-GKAT, an extension of Guarded Kleene Algebra with Tests (GKAT) that adds indicator variables and non-local control flow (goto, break, return). It defines a continuation semantics for CF-GKAT expressions, presents CF-GKAT automata, and shows how to lower these automata to GKAT automata so that trace equivalence can be decided by the existing nearly-linear-time GKAT algorithm. The authors report a Coq formalization of the main theorems and demonstrate the approach on a decompilation case study (Ghidra) and a goto-elimination transformation (Calipso) applied to a function from GNU Coreutils.

Significance. If the printed constructions are corrected, this is a solid and useful contribution: it enlarges the class of programs that can be checked for trace equivalence in nearly linear time, while keeping the decision procedure sound and complete. The explicit reduction to GKAT equivalence is elegant, the machine-checked Coq development is a major strength, and the case study on real control-flow transformations gives evidence of practical applicability. The main caveat is that the paper text currently contains definitional errors in two load-bearing places, so the central algorithm as printed is not yet established.

major comments (3)
  1. [Definition 2.9] The second rule of the sequencing operation copies every trace of G whose continuation lies in {brk_i, acc_i, jmp(ℓ,i)}. Including acc_i is inconsistent with the stated purpose of the rule (preserving non-local control flow) and with the neutrality of labels: with this rule, assert true; assert false would contain the trace α·acc_i, and while true do assert true would spuriously contain α·acc_i via Definition 2.13. The set should be {brk_i, ret, jmp(ℓ,i)} (with the indicator values handled as in the examples), since accepting traces must be composed with H, not copied.
  2. [Definition 3.11] The lowering is not well-defined as printed. The first clause of δ′ resolves a jump only when δ(s,i,α)=jmp(ℓ,i), but Example 3.6 has δ(ŝ,2,{t})=jmp(ℓ,1), so a jump with j≠i arises in the paper's own example. In that case δ′ keeps the jump, and the final 'otherwise' clause of δ↓ returns δ(s,i,α) — also a typo for δ′(s,i,α) — which is a CF-GKAT continuation rather than an element of ⊥+⊤+Σ×(S×I). The intended rule should resolve δ(s,i,α)=jmp(ℓ,j) by λ↓(ℓ,j,α), and δ↓ should use δ′ in its final clause. Since Theorem 3.13 and the equivalence algorithm depend on this construction, the printed definition must be corrected.
  3. [Section 3.5] The restriction of the indicator set to the values occurring in e and f plus one fresh value relies on the claim that if neither i nor i′ appears in e, then ⟦e⟧ℓ_i = ⟦e⟧ℓ_i′ for all labels ℓ. This lemma is stated as 'not hard to show' but is load-bearing for the completeness of the algorithm. Please state it as a lemma and provide a proof or an explicit reference to the corresponding Coq statement.
minor comments (4)
  1. [Definition 2.2 and Example 2.3] Definition 2.2 writes pairs in ⟦−⟧ as (i,α), but Example 2.3 lists ({t1,t2},2), ({t1},2), (∅,2), reversing the order. Please make the notation consistent.
  2. [Section 3.5] The final equivalence chain and the sentence 'Therefore e and f are trace equivalent if and only if equivGKAT(e,f) returns true' should refer to equivCFGKAT, not equivGKAT.
  3. [Section 5.2] In the paragraph on trace equivalence, 'the assignment of x is different at the end of the so' should read 'at the end of the program'.
  4. [Section 4.1] The remark about converting do-while loops says the conversion is admissible when the loop body does not contain break or a label; please clarify whether this condition is checked by the tool or assumed by the front-end.

Circularity Check

0 steps flagged · score 1.0 of 10

No significant circularity: the central derivation reduces CF-GKAT equivalence to GKAT equivalence via proved, Coq-checked Thompson and lowering theorems; self-citations to prior GKAT work are non-load-bearing reuse.

full rationale

The derivation chain in Section 3.5 is explicit: equivCFGKAT(e,f) ⇐⇒ ∀i∈I. equivGKAT(Ae↓i, Af↓i), and the chain then reasons through the external GKAT decidability theorem (Theorem 3.3, cited to Smolka et al. [41]), the lowering theorem (Theorem 3.13), and Thompson's construction (Theorem 3.19). The two new theorems are formalized in Coq via the artifact [51], so the paper's central reductions are machine-checked rather than assumed. The citation to [41] is real independent support: it concerns GKAT automata only, has published proofs, and its assumptions do not include the CF-GKAT target equivalence; co-authorship overlap does not make the reduction circular. No fitted parameter is renamed as a prediction, and trace equivalence is defined independently before the automata construction is proved to preserve it. The self-imposed limitation in the Remark after Definition 2.11 (indicator variables must not occur in primitive tests or actions) is an applicability restriction, not a circular step. The Definition 3.11 jump-resolution typing issue is a correctness and well-definedness concern outside the circularity pass and does not change this verdict.

Assumptions & free parameters 0 free parameters · 5 assumptions · 0 invented entities

The system relies on domain assumptions about the indicator variable's isolation and finiteness, plus the external GKAT decidability result. No free parameters are fitted and no new physical entities are postulated.

assumptions (5)
  • domain assumption The indicator variable x does not occur in any primitive test or primitive action.
    Stated in the Remark after Definition 2.11; necessary for soundness of the continuation semantics, since primitive actions preserve the indicator value and primitive tests do not constrain it.
  • domain assumption The sets of primitive tests, primitive actions, indicator values, and labels are finite.
    Used throughout for decidability and complexity; the algorithm gathers atoms, indicators, and labels from the program.
  • domain assumption Programs are valid: no duplicate labels, no undefined goto targets, no break outside a loop.
    Defined in Section 2.1 as the notion of valid program; the semantics and decision procedure are only for valid programs.
  • standard math GKAT automata equivalence is decidable in nearly linear time (Theorem 3.3).
    Taken from Smolka et al. 2020; the CF-GKAT decision procedure reduces to this external result.
  • ad hoc to paper For a CF-GKAT expression e, if neither indicator value i nor i' appears in e, then the behaviors for i and i' coincide.
    Stated in Section 3.5 as 'not hard to show'; used to justify adding a fresh indicator value * when constructing the alphabet.

how reviews work

0 comments
Cite this review

Pith. "Pith review of CF-GKAT: Efficient Validation of Control-Flow Transformations." pith.science (2026). https://pith.science/paper/PW534WKG

@misc{pith2026241113220,
  author       = {Pith},
  title        = {Pith review of: CF-GKAT: Efficient Validation of Control-Flow Transformations},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/PW534WKG}},
  note         = {Machine review of arXiv:2411.13220}
}
read the original abstract

Guarded Kleene Algebra with Tests (GKAT) provides a sound and complete framework to reason about trace equivalence between simple imperative programs. However, there are still several notable limitations. First, GKAT is completely agnostic with respect to the meaning of primitives, to keep equivalence decidable. Second, GKAT excludes non-local control flow such as goto, break, and return. To overcome these limitations, we introduce Control-Flow GKAT (CF-GKAT), a system that allows reasoning about programs that include non-local control flow as well as hardcoded values. CF-GKAT is able to soundly and completely verify trace equivalence of a larger class of programs, while preserving the nearly-linear efficiency of GKAT. This makes CF-GKAT suitable for the verification of control-flow manipulating procedures, such as decompilation and goto-elimination. To demonstrate CF-GKAT's abilities, we validated the output of several highly non-trivial program transformations, such as Erosa and Hendren's goto-elimination procedure and the output of Ghidra decompiler. CF-GKAT opens up the application of Kleene Algebra to a wider set of challenges, and provides an important verification tool that can be applied to the field of decompilation and control-flow transformation.

Figures

Figures reproduced from arXiv: 2411.13220 by the authors.

Figure 1
Figure 1. Different versions of mp_factor_using_pollard_rho in factor.c, part of GNU Coreutils. Proc. ACM Program. Lang., Vol. 9, No. POPL, Article 21. Publication date: January 2025 [PITH_FULL_IMAGE:figures/full_fig_p020_1.png] view at source ↗
Figure 2
Figure 2. Different versions of mp_factor_using_pollard_rho in factor.c, part of GNU Coreutils. Proc. ACM Program. Lang., Vol. 9, No. POPL, Article 21. Publication date: January 2025 [PITH_FULL_IMAGE:figures/full_fig_p021_2.png] view at source ↗
Figure 3
Figure 3. Plot of the number of blinded functions per cyclomatic complexity number (CCN). The maximum [PITH_FULL_IMAGE:figures/full_fig_p023_3.png] view at source ↗

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

52 extracted references · 22 canonical work pages

  1. [1]

    Kamal Aboul-Hosn and Dexter Kozen. 2008. Local variable scoping and Kleene algebra with tests. J. Log. Algebraic Methods Program. 76, 1 (2008), 3–17. https://doi.org/10.1016/J.JLAP.2007.10.007

    work page doi:10.1016/j.jlap.2007.10.007 2008

  2. [2]

    Carolyn Jane Anderson, Nate Foster, Arjun Guha, Jean-Baptiste Jeannin, Dexter Kozen, Cole Schlesinger, and David Walker. 2014. NetKAT: semantic foundations for networks. InPOPL. 113–126. https://doi.org/10.1145/2535838.2535862

    arXiv 2014

  3. [3]

    Allegra Angus and Dexter Kozen. 2001. Kleene Algebra with Tests and Program Schematology . Technical Report TR2001-1844. Cornell University

    work page 2001

  4. [4]

    Cheng Zhang Arthur Azevedo de Amorim and Marco Gaboardi. 2024. Kleene Algebra with Commutativity Conditions Is Undecidable. https://hal.science/hal-04534715v2 Proc. ACM Program. Lang., Vol. 9, No. POPL, Article 21. Publication date: January 2025. 21:26 Cheng Zhang, Tobias Kappé, David E. Narváez, and Nico Naus

    work page 2024

  5. [5]

    Payas Awadhutkar, Ahmed Tamrawi, Ryan Goluch, and Suresh C. Kothari. 2022. Control flow equivalence method for establishing sanctity of compiling. Comput. Secur. 115 (2022), 102608. https://doi.org/10.1016/J.COSE.2022.102608

    work page arXiv 2022

  6. [6]

    Millstein, and Sriram K

    Thomas Ball, Rupak Majumdar, Todd D. Millstein, and Sriram K. Rajamani. 2001. Automatic Predicate Abstraction of C Programs. In PLDI. 203–213. https://doi.org/10.1145/378795.378846

    arXiv 2001

  7. [7]

    Corrado Böhm and Giuseppe Jacopini. 1966. Flow diagrams, Turing machines and languages with only two formation rules. Commun. ACM 9, 5 (1966), 366–371. https://doi.org/10.1145/355592.365646

    arXiv 1966

  8. [8]

    Brzozowski

    Janusz A. Brzozowski. 1964. Derivatives of Regular Expressions. J. ACM 11, 4 (1964), 481–494. https://doi.org/10.1145/ 321239.321249

    arXiv 1964

Show all 52 references
  1. [9]

    Ying Cao, Runze Zhang, Ruigang Liang, and Kai Chen. 2024. Evaluating the Effectiveness of Decompilers. In ISSTA. ACM, 491–502. https://doi.org/10.1145/3650212.3652144

    2024

  2. [10]

    Hugues Cassé, Louis Féraud, Christine Rochange, and Pascal Sainrat. 2002. Une approche pour réduire la complexité du flot de contrôle dans les programmes C. Tech. Sci. Informatiques 21, 7 (2002), 1009–1032. http://tsi.revuesonline. com/article.jsp?articleId=3831

    2002

  3. [11]

    Junjie Chen, Jibesh Patra, Michael Pradel, Yingfei Xiong, Hongyu Zhang, Dan Hao, and Lu Zhang. 2021. A Survey of Compiler Testing. ACM Comput. Surv. 53, 1 (2021), 4:1–4:36. https://doi.org/10.1145/3363562

    2021 doi

  4. [12]

    Cristina Cifuentes. 1994. Reverse compilation techniques. Ph. D. Dissertation. Queensland University of Technology

    1994

  5. [13]

    Ernie Cohen, Dexter Kozen, and Frederick Smith. 1996. The Complexity of Kleene Algebra with Tests . Technical Report TR96-1598

    1996

  6. [14]

    Coq Development Team. 2022. The Coq Reference Manual, version 8.15. Available electronically at http://coq.inria.fr/doc

    2022

  7. [15]

    Adve, and Christopher W

    Sandeep Dasgupta, Sushant Dinesh, Deepan Venkatesh, Vikram S. Adve, and Christopher W. Fletcher. 2020. Scalable validation of binary lifters. In PLDI. 655–671. https://doi.org/10.1145/3385412.3385964

    2020

  8. [16]

    Erosa and Laurie J

    Ana M. Erosa and Laurie J. Hendren. 1994. Taming Control Flow: A Structured Approach to Eliminating Goto Statements. In ICCL. IEEE Computer Society, 229–240. https://doi.org/10.1109/ICCL.1994.288377

    1994

  9. [17]

    Murdoch James Gabbay and Vincenzo Ciancia. 2011. Freshness and Name-Restriction in Sets of Traces with Names. In FoSSaCS. 365–380. https://doi.org/10.1007/978-3-642-19805-2_25

    2011 doi

  10. [18]

    Zuck, and Clark W

    Benjamin Goldberg, Lenore D. Zuck, and Clark W. Barrett. 2004. Into the Loops: Practical Issues in Translation Validation for Optimizing Compilers. In COCV@ETAPS. 53–71. https://doi.org/10.1016/J.ENTCS.2005.01.030

    2004 doi

  11. [19]

    Niels Bjørn Bugge Grathwohl, Dexter Kozen, and Konstantinos Mamouras. 2014. KAT + B!. In CSL-LICS. ACM, 44:1–44:10. https://doi.org/10.1145/2603088.2603095

    2014

  12. [20]

    Theodoros Kasampalis. 2021. Translation validation for compilation verification . Ph. D. Dissertation. University of Illinois Urbana-Champaign, USA. https://hdl.handle.net/2142/110460

    2021

  13. [21]

    Adve, and Grigore Rosu

    Theodoros Kasampalis, Daejun Park, Zhengyao Lin, Vikram S. Adve, and Grigore Rosu. 2021. Language-parametric compiler validation with application to LLVM. In ASPLOS. ACM, 1004–1019. https://doi.org/10.1145/3445814.3446751

    2021

  14. [22]

    Dexter Kozen. 1996. Kleene algebra with tests and commutativity conditions. In TACAS. 14–33. https://doi.org/10. 1007/3-540-61042-1_35

    1996

  15. [23]

    Dexter Kozen. 2008. Nonlocal Flow of Control and Kleene Algebra with Tests. In LICS. 105–117. https://doi.org/10. 1109/LICS.2008.32

    2008

  16. [24]

    Dexter Kozen, Konstantinos Mamouras, Daniela Petrisan, and Alexandra Silva. 2015. Nominal Kleene Coalgebra. In ICALP. 286–298. https://doi.org/10.1007/978-3-662-47666-6_23

    2015 doi

  17. [25]

    Dexter Kozen, Konstantinos Mamouras, and Alexandra Silva. 2017. Completeness and incompleteness in nominal Kleene algebra. J. Log. Algebraic Methods Program. 91, 17–32. https://doi.org/10.1016/J.JLAMP.2017.06.002

    2017 doi

  18. [26]

    Dexter Kozen and Maria-Christina Patron. 2000. Certification of Compiler Optimizations Using Kleene Algebra with Tests. In CL. 568–582. https://doi.org/10.1007/3-540-44957-4_38

    2000 doi

  19. [27]

    Dexter Kozen and Frederick Smith. 1996. Kleene Algebra with Tests: Completeness and Decidability. In CSL. 244–259. https://doi.org/10.1007/3-540-63172-0_43

    1996 doi

  20. [28]

    Dexter Kozen and Wei-Lung Dustin Tseng. 2008. The Böhm-Jacopini Theorem Is False, Propositionally. In MPC. 177–192. https://doi.org/10.1007/978-3-540-70594-9_11

    2008 doi

  21. [29]

    Kuznetsov

    Stepan L. Kuznetsov. 2023. On the Complexity of Reasoning in Kleene Algebra with Commutativity Conditions. In ICTAC. 83–99. https://doi.org/10.1007/978-3-031-47963-2_7

    2023 doi

  22. [30]

    Vu Le, Mehrdad Afshari, and Zhendong Su. 2014. Compiler validation via equivalence modulo inputs. In PLDI. ACM, 216–226. https://doi.org/10.1145/2594291.2594334

    2014

  23. [31]

    Xavier Leroy, Sandrine Blazy, Daniel Kästner, Bernhard Schommer, Markus Pister, and Christian Ferdinand. 2016. CompCert – A Formally Verified Optimizing Compiler. In ERTS

    2016

  24. [32]

    Zhibo Liu and Shuai Wang. 2020. How far we have come: testing decompilation correctness of C decompilers. InISSTA. ACM, 475–487. https://doi.org/10.1145/3395363.3397370

    2020

  25. [33]

    T.J. McCabe. 1976. A Complexity Measure. IEEE Transactions on Software Engineering SE-2, 4 (1976), 308–320. https://doi.org/10.1109/TSE.1976.233837 Proc. ACM Program. Lang., Vol. 9, No. POPL, Article 21. Publication date: January 2025. CF-GKAT: Efficient Validation of Control-...

    1976

  26. [34]

    Mark Moeller, Jules Jacobs, Olivier Savary Bélanger, David Darais, Cole Schlesinger, Steffen Smolka, Nate Foster, and Alexandra Silva. 2024. KATch: A Fast Symbolic Verifier for NetKAT. InPLDI. 1905–1928. https://doi.org/10.1145/3656454

    2024 doi

  27. [35]

    George C. Necula. 2000. Translation validation for an optimizing compiler. In PLDI. ACM, 83–94. https://doi.org/10. 1145/349299.349314

    2000

  28. [36]

    Georg Neis, Chung-Kil Hur, Jan-Oliver Kaiser, Craig McLaughlin, Derek Dreyer, and Viktor Vafeiadis. 2015. Pilsner: a compositionally verified compiler for a higher-order imperative language. In ICFP. ACM, 166–178. https://doi.org/10. 1145/2784731.2784764

    2015

  29. [37]

    Amir Pnueli, Michael Siegel, and Eli Singerman. 1998. Translation Validation. In TACAS. 151–166. https://doi.org/10. 1007/BFB0054170

    1998

  30. [38]

    Damien Pous. 2015. Symbolic Algorithms for Language Equivalence and Kleene Algebra with Tests. In POPL. 357–368. https://doi.org/10.1145/2676726.2677007

    2015

  31. [39]

    Todd Schmid, Tobias Kappé, Dexter Kozen, and Alexandra Silva. 2021. Guarded Kleene Algebra with Tests: Coequations, Coinduction, and Completeness. , 142:1–142:14 pages. https://doi.org/10.4230/LIPICS.ICALP.2021.142

    2021 doi

  32. [40]

    Myreen, and Gerwin Klein

    Thomas Arthur Leck Sewell, Magnus O. Myreen, and Gerwin Klein. 2013. Translation validation for a verified OS kernel. In PLDI. ACM, 471–482. https://doi.org/10.1145/2491956.2462183

    2013

  33. [41]

    Steffen Smolka, Nate Foster, Justin Hsu, Tobias Kappé, Dexter Kozen, and Alexandra Silva. 2020. Guarded Kleene algebra with tests: verification of uninterpreted programs in nearly linear time. In POPL. 61:1–61:28. https://doi.org/ 10.1145/3371129

    2020 doi

  34. [42]

    Myreen, Ramana Kumar, Anthony C

    Yong Kiam Tan, Magnus O. Myreen, Ramana Kumar, Anthony C. J. Fox, Scott Owens, and Michael Norrish. 2016. A new verified compiler backend for CakeML. In ICFP. ACM, 60–73. https://doi.org/10.1145/2951913.2951924

    2016

  35. [43]

    Robert Endre Tarjan. 1975. Efficiency of a Good But Not Linear Set Union Algorithm. J. ACM 22, 2 (1975), 215–225. https://doi.org/10.1145/321879.321884

    1975

  36. [44]

    Balder ten Cate and Tobias Kappé. 2025. Algebras for Deterministic Computation are Inherently Incomplete. In POPL. 25:1–25:27. https://doi.org/10.1145/3704861

    2025 doi

  37. [45]

    Ken Thompson. 1968. Regular Expression Search Algorithm. Commun. ACM 11, 6 (1968), 419–422. https://doi.org/10. 1145/363347.363387

    1968

  38. [46]

    Bockenek, Zhoulai Fu, and Binoy Ravindran

    Freek Verbeek, Joshua A. Bockenek, Zhoulai Fu, and Binoy Ravindran. 2022. Formally verified lifting of C-compiled x86-64 binaries. In PLDI. ACM, 934–949. https://doi.org/10.1145/3519939.3523702

    2022

  39. [47]

    Freek Verbeek, Nico Naus, and Binoy Ravindran. 2024. Verifiably Correct Lifting of Position-Independent x86-64 Binaries to Symbolized Assembly. In CCS

    2024

  40. [48]

    Freek Verbeek, Pierre Olivier, and Binoy Ravindran. 2020. Sound C Code Decompilation for a Subset of x86-64 Binaries. In SEFM. 247–264. https://doi.org/10.1007/978-3-030-58768-0_14

    2020 doi

  41. [49]

    Khaled Yakdan, Sebastian Eschweiler, Elmar Gerhards-Padilla, and Matthew Smith. 2015. No More Gotos: De- compilation Using Pattern-Independent Control-Flow Structuring and Semantic-Preserving Transformations. In NDSS. https://www.ndss-symposium.org/ndss2015/no-more-gotos-decom...

    2015

  42. [50]

    Xuejun Yang, Yang Chen, Eric Eide, and John Regehr. 2011. Finding and understanding bugs in C compilers. In PLDI. ACM, 283–294. https://doi.org/10.1145/1993498.1993532

    2011

  43. [51]

    Narvaéz, and Nico Naus

    Cheng Zhang, Tobias Kappé, David E. Narvaéz, and Nico Naus. 2024. CF-GKAT: Efficient Validation of Control-Flow Transformations (Artifact). https://doi.org/10.5281/zenodo.13938565

    2024 doi

  44. [52]

    Yiji Zhang and Lenore D. Zuck. 2018. Formal Verification of Optimizing Compilers. In ICDCIT. 50–65. https: //doi.org/10.1007/978-3-319-72344-0_3 Received 2024-07-11; accepted 2024-11-07 Proc. ACM Program. Lang., Vol. 9, No. POPL, Article 21. Publication date: January 2025

    2018 doi

Pith tools

Reviewed August 12, 2026 · model on record in the stance chip above.