pith. sign in

arxiv: 2607.00563 · v1 · pith:CQHIX5UPnew · submitted 2026-07-01 · 💻 cs.PL

Certificate-Carrying Transformation of Event-Driven Block Programs

Yuan Si , Jialu Zhang This is my paper

Pith reviewed 2026-07-02 02:17 UTC · model grok-4.3

classification 💻 cs.PL
keywords block-based languagessource-to-source rewritingbehavior preservationcertificate-carrying transformationevent-driven programsoptimization verificationScratch
0
0 comments X

The pith

A trusted checker recomputes every side condition of a proposed rewrite, ensuring an optimizer bug cannot mint an unsound acceptance under stated model-to-VM assumptions.

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

The paper establishes that optimization of event-driven block programs can be turned into certificate-carrying source-to-source rewriting. An untrusted optimizer proposes a rewrite while a trusted fail-closed checker accepts it only after recomputing all required side conditions under an explicit observation lens. This approach keeps the trusted computing base small because the checker alone decides acceptance. The central soundness result is a cooperative-frame refinement theorem, mechanized in Lean, that justifies when a write can be removed without changing observable behavior. Evaluation on 300 Scratch projects shows the checker accepts valid rewrites on 94.3 percent of cases, runs in under a tenth of a second, and rejects all 4,278 adversarial perturbations tested.

Core claim

We turn optimization into certificate-carrying source-to-source rewriting. An untrusted optimizer proposes a rewrite; a trusted, fail-closed checker accepts it only after recomputing every side condition that the rewrite's behavior preservation depends on under an explicit observation lens. The checker is the sole authority: given a correct checker and a small, explicitly stated set of model-to-VM assumptions, an optimizer bug cannot mint an unsound acceptance. The observation lens is a parameter, and the central soundness argument is a cooperative-frame refinement theorem: a write overwritten before any thread observes it, within a window in which no thread yields, can be removed. We mechan

What carries the argument

The cooperative-frame refinement theorem under a parametric observation lens, which justifies removing a write that is overwritten before observation within a non-yielding window.

If this is right

  • The checker accepts a behavior-preserving rewrite on 94.3% of 300 real Scratch projects.
  • Certification costs under one tenth of a second per project.
  • A cross-family adversarial campaign of 4,278 perturbed rewrites produces zero false accepts.
  • An ablation that removes semantic side conditions ships rewrites the virtual machine confirms change behavior, while the full checker rejects every one.

Where Pith is reading between the lines

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

  • The same parametric theorem structure could be instantiated for additional rewrite families beyond the six evaluated.
  • The approach may transfer to other concurrent event-driven languages that share similar observation models.
  • Small trusted checkers of this form could support verified transformations in other end-user programming environments.

Load-bearing premise

The model-to-VM assumptions accurately capture the observable semantics of the target virtual machine and the chosen observation lens detects all behavior changes relevant to the rewrite families.

What would settle it

A rewrite that the checker accepts but that the virtual machine confirms changes observable behavior under the stated observation lens would falsify the central claim.

Figures

Figures reproduced from arXiv: 2607.00563 by Jialu Zhang, Yuan Si.

Figure 1
Figure 1. Figure 1: The optimizer proposes a rewrite with a certificate; the checker [PITH_FULL_IMAGE:figures/full_fig_p003_1.png] view at source ↗
read the original abstract

Block-based end-user languages such as Scratch run tens of millions of programs. Existing tools establish behavior preservation through program analysis and testing without a checked guarantee. We turn optimization into certificate-carrying source-to-source rewriting. An untrusted optimizer proposes a rewrite; a trusted, fail-closed checker accepts it only after recomputing every side condition that the rewrite's behavior preservation depends on under an explicit observation lens. The checker is the sole authority: given a correct checker and a small, explicitly stated set of model-to-VM assumptions, an optimizer bug cannot mint an unsound acceptance. The observation lens is a parameter, and the central soundness argument is a cooperative-frame refinement theorem: a write overwritten before any thread observes it, within a window in which no thread yields, can be removed. We mechanize this theorem in Lean and show that one parametric statement covers two concrete rewrite families instantiated to variable state and renderer state. We build a checker for six rewrite families and evaluate it on 300 real Scratch projects. The checker accepts a behavior-preserving rewrite on 94.3% of projects (283 of 300); certification costs under one tenth of a second per project; and a cross-family adversarial campaign of 4,278 perturbed rewrites produces zero false accepts. An audit found eight false accepts the per-family test suites missed; each is now rejected. An ablation that strips the semantic side conditions, leaving analysis and testing alone, ships rewrites the virtual machine confirms change behavior; the full checker rejects every one. The result shows how to provide behavior-preservation guarantees for a concurrent, event-driven, end-user language. The checker recomputes every required condition instead of trusting optimizer claims, keeping the trusted base small.

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

1 major / 0 minor

Summary. The paper presents certificate-carrying source-to-source rewriting for optimizing event-driven block programs in languages such as Scratch. An untrusted optimizer proposes rewrites that a trusted fail-closed checker accepts only after recomputing all side conditions under an explicit observation lens. The central soundness argument is a cooperative-frame refinement theorem mechanized in Lean, shown to cover two rewrite families (variable state and renderer state); a checker is implemented for six families total. Evaluation on 300 real projects reports 94.3% acceptance of behavior-preserving rewrites, sub-0.1s certification time, and zero false accepts across 4,278 adversarial perturbations. An ablation and audit further support the approach.

Significance. If the result holds, the work shows how to obtain behavior-preservation guarantees for concurrent event-driven end-user languages while keeping the trusted base small. Strengths include the Lean-mechanized theorem, explicit model-to-VM assumptions, an adversarial test suite with zero false accepts, and an ablation demonstrating that semantic side conditions are necessary. The result is relevant to verified compilation and optimization for block-based languages.

major comments (1)
  1. [abstract and sections describing the theorem and checker implementation] The cooperative-frame refinement theorem is mechanized in Lean and shown to cover only two of the six rewrite families for which the checker is built and on which the evaluation and adversarial campaign (4,278 rewrites) are performed. For the remaining four families the claim that recomputed side conditions suffice for behavior preservation therefore rests on unmechanized arguments; an error in those arguments would allow the checker to accept unsound rewrites, so the "given a correct checker" guarantee does not extend to the full set of families used in the reported results.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the careful and constructive review. The observation about the scope of the mechanized theorem is accurate, and we address it directly below.

read point-by-point responses

  1. Referee: [abstract and sections describing the theorem and checker implementation] The cooperative-frame refinement theorem is mechanized in Lean and shown to cover only two of the six rewrite families for which the checker is built and on which the evaluation and adversarial campaign (4,278 rewrites) are performed. For the remaining four families the claim that recomputed side conditions suffice for behavior preservation therefore rests on unmechanized arguments; an error in those arguments would allow the checker to accept unsound rewrites, so the "given a correct checker" guarantee does not extend to the full set of families used in the reported results.

    Authors: We agree with the referee's assessment. The Lean mechanization establishes the cooperative-frame refinement theorem parametrically and instantiates it only for the variable-state and renderer-state families. The checker for the remaining four families (and the reported evaluation results) relies on pen-and-paper arguments that the same frame condition, once the side conditions are re-checked, suffices for those state models. An error in those arguments would indeed weaken the end-to-end guarantee for those families. In the revised manuscript we will add an explicit table enumerating the mechanization status of each of the six families, qualify the abstract and introduction to distinguish the mechanized core from the manually justified families, and note that the adversarial campaign and ablation still supply empirical evidence even for the unmechanized cases. We do not claim that the mechanized theorem alone covers all six families. revision: yes

Circularity Check

0 steps flagged

No significant circularity; soundness rests on mechanized theorem and explicit assumptions

full rationale

The paper's central claim is that a correct checker plus explicitly stated model-to-VM assumptions prevents unsound acceptances. The cooperative-frame refinement theorem is mechanized in Lean as an independent artifact and is presented as covering two of the six rewrite families via a single parametric statement; the checker for all six recomputes side conditions rather than trusting optimizer output. No derivation step reduces by construction to a fitted parameter, self-citation, or self-definition (e.g., no quantity is defined in terms of the result it is used to predict). The Lean mechanization supplies external, machine-checked support outside the paper's own equations, so the argument remains self-contained against the stated assumptions.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The central claim rests on the cooperative-frame refinement theorem (mechanized in Lean) and the model-to-VM assumptions; no free parameters or invented entities are introduced.

axioms (1)
  • domain assumption The model-to-VM assumptions accurately reflect the observable behavior of the Scratch virtual machine.
    Soundness of the checker depends on these assumptions holding for the target VM.

pith-pipeline@v0.9.1-grok · 5834 in / 1433 out tokens · 31843 ms · 2026-07-02T02:17:52.828646+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

61 extracted references · 61 canonical work pages · 3 internal anchors

  1. [1]

    Understanding recurring quality prob- lems and their impact on code sharing in block-based software,

    P. Techapalokul and E. Tilevich, “Understanding recurring quality prob- lems and their impact on code sharing in block-based software,” inIEEE Symp. Visual Languages and Human-Centric Computing (VL/HCC), 2017, pp. 43–51

    work page 2017

  2. [2]

    Software clones in Scratch projects: On the presence of copy-and-paste in compu- tational thinking learning,

    G. Robles, J. Moreno-Le ´on, E. Aivaloglou, and F. Hermans, “Software clones in Scratch projects: On the presence of copy-and-paste in compu- tational thinking learning,” inIEEE Int. Workshop on Software Clones (IWSC), 2017, pp. 31–37

    work page 2017

  3. [3]

    Formal verification of a realistic compiler,

    X. Leroy, “Formal verification of a realistic compiler,”Communications of the ACM, vol. 52, no. 7, pp. 107–115, 2009

    work page 2009

  4. [4]

    A formally verified compiler back-end,

    ——, “A formally verified compiler back-end,”Journal of Automated Reasoning, vol. 43, no. 4, pp. 363–446, 2009

    work page 2009

  5. [5]

    Translation validation,

    A. Pnueli, M. Siegel, and E. Singerman, “Translation validation,” in Tools and Algorithms for the Construction and Analysis of Systems (TACAS), ser. LNCS 1384, 1998, pp. 151–166

    work page 1998

  6. [6]

    Translation validation for an optimizing compiler,

    G. C. Necula, “Translation validation for an optimizing compiler,” inProc. ACM SIGPLAN Conf. Programming Language Design and Implementation (PLDI), 2000, pp. 83–94

    work page 2000

  7. [7]

    Alive2: Bounded translation validation for LLVM,

    N. P. Lopes, J. Lee, C.-K. Hur, Z. Liu, and J. Regehr, “Alive2: Bounded translation validation for LLVM,” inProc. ACM SIGPLAN Conf. Pro- gramming Language Design and Implementation (PLDI), 2021, pp. 65– 79

    work page 2021

  8. [8]

    Code quality improvement for all: Automated refactoring for Scratch,

    P. Techapalokul and E. Tilevich, “Code quality improvement for all: Automated refactoring for Scratch,” inIEEE Symp. Visual Languages and Human-Centric Computing (VL/HCC), 2019, pp. 117–125

    work page 2019

  9. [9]

    Improving readability of Scratch programs with search-based refactoring,

    F. Adler, G. Fraser, E. Gr ¨undinger, N. K ¨orber, S. Labrenz, J. Lerchen- berger, S. Lukasczyk, and S. Schweikl, “Improving readability of Scratch programs with search-based refactoring,” inIEEE Int. Working Conf. Source Code Analysis and Manipulation (SCAM), 2021, pp. 120–130

    work page 2021

  10. [10]

    The Scratch programming language and environment,

    J. Maloney, M. Resnick, N. Rusk, B. Silverman, and E. Eastmond, “The Scratch programming language and environment,”ACM Transactions on Computing Education, vol. 10, no. 4, pp. 16:1–16:15, 2010

    work page 2010

  11. [11]

    Scratch: Programming for all,

    M. Resnick, J. Maloney, A. Monroy-Hern ´andez, N. Rusk, E. Eastmond, K. Brennan, A. Millner, E. Rosenbaum, J. Silver, B. Silverman, and Y . Kafai, “Scratch: Programming for all,”Communications of the ACM, vol. 52, no. 11, pp. 60–67, 2009

    work page 2009

  12. [12]

    The Lean 4 theorem prover and program- ming language,

    L. de Moura and S. Ullrich, “The Lean 4 theorem prover and program- ming language,” inAutomated Deduction (CADE), ser. LNCS 12699, 2021, pp. 625–635

    work page 2021

  13. [13]

    Equality saturation: A new approach to optimization,

    R. Tate, M. Stepp, Z. Tatlock, and S. Lerner, “Equality saturation: A new approach to optimization,” inProc. ACM SIGPLAN-SIGACT Symp. Principles of Programming Languages (POPL), 2009, pp. 264–276

    work page 2009

  14. [14]

    egg: Fast and extensible equality saturation,

    M. Willsey, C. Nandi, Y . R. Wang, O. Flatt, Z. Tatlock, and P. Panchekha, “egg: Fast and extensible equality saturation,” inProc. ACM SIGPLAN- SIGACT Symp. Principles of Programming Languages (POPL), vol. 5, 2021, pp. 1–29

    work page 2021

  15. [15]

    Ehrig, K

    H. Ehrig, K. Ehrig, U. Prange, and G. Taentzer,Fundamentals of Algebraic Graph Transformation. Springer, 2006

    work page 2006

  16. [16]

    ScratchLens: Lens-Parametric Behavioral Equivalence for Scratch Programs

    Y . Si and J. Zhang, “ScratchLens: Lens-parametric behavioral equivalence for Scratch programs,” 2026. [Online]. Available: https: //arxiv.org/abs/2606.15817

    work page internal anchor Pith review Pith/arXiv arXiv 2026

  17. [17]

    CakeML: A verified implementation of ML,

    R. Kumar, M. O. Myreen, M. Norrish, and S. Owens, “CakeML: A verified implementation of ML,” inProc. ACM SIGPLAN-SIGACT Symp. Principles of Programming Languages (POPL), 2014, pp. 179– 192

    work page 2014

  18. [18]

    Compositional CompCert,

    G. Stewart, L. Beringer, S. Cu ´ellar, and A. W. Appel, “Compositional CompCert,” inProc. ACM SIGPLAN-SIGACT Symp. Principles of Programming Languages (POPL), 2015, pp. 275–287

    work page 2015

  19. [19]

    Verified software toolchain,

    A. W. Appel, “Verified software toolchain,” inProc. European Symp. Programming (ESOP), ser. LNCS 6602, 2011, pp. 1–17

    work page 2011

  20. [20]

    VOC: A methodology for the translation validation of optimizing compilers,

    L. Zuck, A. Pnueli, Y . Fang, and B. Goldberg, “VOC: A methodology for the translation validation of optimizing compilers,”Journal of Universal Computer Science, vol. 9, no. 3, pp. 223–247, 2003

    work page 2003

  21. [21]

    TVOC: A translation validator for optimizing compilers,

    C. Barrett, Y . Fang, B. Goldberg, Y . Hu, A. Pnueli, and L. Zuck, “TVOC: A translation validator for optimizing compilers,” inComputer Aided Verification (CAV), ser. LNCS 3576, 2005, pp. 291–295

    work page 2005

  22. [22]

    Formal verification of translation valida- tors: A case study on instruction scheduling optimizations,

    J.-B. Tristan and X. Leroy, “Formal verification of translation valida- tors: A case study on instruction scheduling optimizations,” inProc. ACM SIGPLAN-SIGACT Symp. Principles of Programming Languages (POPL), 2008, pp. 17–27

    work page 2008

  23. [23]

    Verified validation of lazy code motion,

    ——, “Verified validation of lazy code motion,” inProc. ACM SIGPLAN Conf. Programming Language Design and Implementation (PLDI), 2009, pp. 316–326

    work page 2009

  24. [24]

    Verified peephole optimizations for CompCert,

    E. Mullen, D. Zuniga, Z. Tatlock, and D. Grossman, “Verified peephole optimizations for CompCert,” inProc. ACM SIGPLAN Conf. Program- ming Language Design and Implementation (PLDI), 2016, pp. 448–461

    work page 2016

  25. [25]

    Provably correct peephole optimizations with Alive,

    N. P. Lopes, D. Menendez, S. Nagarakatte, and J. Regehr, “Provably correct peephole optimizations with Alive,” inProc. ACM SIGPLAN Conf. Programming Language Design and Implementation (PLDI), 2015, pp. 22–32

    work page 2015

  26. [26]

    Automatically proving the correctness of compiler optimizations,

    S. Lerner, T. Millstein, and C. Chambers, “Automatically proving the correctness of compiler optimizations,” inProc. ACM SIGPLAN Conf. Programming Language Design and Implementation (PLDI), 2003, pp. 220–231

    work page 2003

  27. [27]

    Credible compilation,

    M. Rinard, “Credible compilation,” Massachusetts Institute of Technol- ogy, Tech. Rep. MIT-LCS-TR-776, 1999

    work page 1999

  28. [28]

    Witnessing program transformations,

    K. S. Namjoshi and L. D. Zuck, “Witnessing program transformations,” inStatic Analysis Symposium (SAS), ser. LNCS 7935, 2013, pp. 304– 323

    work page 2013

  29. [29]

    Crellvm: Verified credible compilation for LLVM,

    J. Kang, Y . Kim, Y . Song, J. Lee, S. Park, M. D. Shin, Y . Kim, S. Cho, J. Choi, C.-K. Hur, and K. Yi, “Crellvm: Verified credible compilation for LLVM,” inProc. ACM SIGPLAN Conf. Programming Language Design and Implementation (PLDI), 2018, pp. 631–645

    work page 2018

  30. [30]

    Equality-based translation validator for LLVM,

    M. Stepp, R. Tate, and S. Lerner, “Equality-based translation validator for LLVM,” inComputer Aided Verification (CAV), ser. LNCS 6806, 2011, pp. 737–742

    work page 2011

  31. [31]

    CompCertTSO: A verified compiler for relaxed-memory concurrency,

    J. ˇSevˇc´ık, V . Vafeiadis, F. Zappa Nardelli, S. Jagannathan, and P. Sewell, “CompCertTSO: A verified compiler for relaxed-memory concurrency,” Journal of the ACM, vol. 60, no. 3, pp. 22:1–22:50, 2013

    work page 2013

  32. [32]

    Proof-carrying code,

    G. C. Necula, “Proof-carrying code,” inProc. ACM SIGPLAN-SIGACT Symp. Principles of Programming Languages (POPL), 1997, pp. 106– 119

    work page 1997

  33. [33]

    seL4: Formal verification of an OS kernel,

    G. Klein, K. Elphinstone, G. Heiser, J. Andronick, D. Cock, P. Derrin, D. Elkaduwe, K. Engelhardt, R. Kolanski, M. Norrish, T. Sewell, H. Tuch, and S. Winwood, “seL4: Formal verification of an OS kernel,” inProc. ACM SIGOPS Symp. Operating Systems Principles (SOSP), 2009, pp. 207–220

    work page 2009

  34. [34]

    The Esterel synchronous programming language: Design, semantics, implementation,

    G. Berry and G. Gonthier, “The Esterel synchronous programming language: Design, semantics, implementation,”Science of Computer Programming, vol. 19, no. 2, pp. 87–152, 1992

    work page 1992

  35. [35]

    The synchronous data flow programming language LUSTRE,

    N. Halbwachs, P. Caspi, P. Raymond, and D. Pilaud, “The synchronous data flow programming language LUSTRE,”Proceedings of the IEEE, vol. 79, no. 9, pp. 1305–1320, 1991

    work page 1991

  36. [36]

    A formally verified compiler for Lustre,

    T. Bourke, L. Brun, P.- ´E. Dagand, X. Leroy, M. Pouzet, and L. Rieg, “A formally verified compiler for Lustre,” inProc. ACM SIGPLAN Conf. Programming Language Design and Implementation (PLDI), 2017, pp. 586–601

    work page 2017

  37. [37]

    A dataset of Scratch programs: Scraped, shaped and scored,

    E. Aivaloglou, F. Hermans, J. Moreno-Le ´on, and G. Robles, “A dataset of Scratch programs: Scraped, shaped and scored,” inProc. Int. Conf. Mining Software Repositories (MSR), 2017, pp. 511–514

    work page 2017

  38. [38]

    How kids code and how we know: An exploratory study on the Scratch repository,

    E. Aivaloglou and F. Hermans, “How kids code and how we know: An exploratory study on the Scratch repository,” inProc. ACM Conf. International Computing Education Research (ICER), 2016, pp. 53–61

    work page 2016

  39. [39]

    Hairball: Lint-inspired static analysis of Scratch projects,

    B. Boe, C. Hill, M. Len, G. Dreschler, P. Conrad, and D. Franklin, “Hairball: Lint-inspired static analysis of Scratch projects,” inProc. ACM Technical Symp. Computer Science Education (SIGCSE), 2013, pp. 215–220

    work page 2013

  40. [40]

    Common bugs in Scratch programs,

    C. Fr ¨adrich, F. Oberm ¨uller, N. K ¨orber, U. Heuer, and G. Fraser, “Common bugs in Scratch programs,” inProc. ACM Conf. Innovation and Technology in Computer Science Education (ITiCSE), 2020, pp. 89–95

    work page 2020

  41. [41]

    Testing scratch programs automatically,

    A. Stahlbauer, M. Kreis, and G. Fraser, “Testing scratch programs automatically,” inProc. ACM Joint European Software Engineering Conf. and Symp. Foundations of Software Engineering (ESEC/FSE), 2019, pp. 165–175

    work page 2019

  42. [42]

    arXiv preprint arXiv:2509.11065

    Y . Si, D. Li, H. Shi, and J. Zhang, “ViScratch: Using large language models and gameplay videos for automated feedback in Scratch,” arXiv:2509.11065 [cs.SE], 2025

    work page arXiv 2025

  43. [43]

    Stitch: Step-by-step LLM guided tutoring for Scratch,

    Y . Si, K. Qi, D. Li, H. Shi, and J. Zhang, “Stitch: Step-by-step LLM guided tutoring for Scratch,” arXiv:2510.26634 [cs.SE], 2025

    work page arXiv 2025

  44. [44]

    ScratchEval: A multi- modal evaluation framework for LLMs in block-based programming,

    Y . Si, S. Han, D. Li, H. Shi, and J. Zhang, “ScratchEval: A multi- modal evaluation framework for LLMs in block-based programming,” arXiv:2602.00757 [cs.SE], 2026

    work page arXiv 2026

  45. [45]

    EcoScratch: Cost- effective multimodal repair for Scratch using execution feedback,

    Y . Si, M. Wang, D. Li, H. Shi, and J. Zhang, “EcoScratch: Cost- effective multimodal repair for Scratch using execution feedback,” arXiv:2603.29624 [cs.SE], 2026

    work page arXiv 2026

  46. [46]

    Raven: Rethinking Automated Assessment for Scratch Programs via Video-Grounded Evaluation

    D. Li, D. Li, H. Shi, and J. Zhang, “Raven: Rethinking auto- mated assessment for Scratch programs via video-grounded evaluation,” arXiv:2604.17820 [cs.SE], 2026

    work page internal anchor Pith review Pith/arXiv arXiv 2026

  47. [47]

    ScratchWorld: Evaluating If World Models Compute Executable Consequences

    Y . Lin and J. Zhang, “ScratchWorld: Evaluating if world models compute executable consequences,” arXiv:2606.31689 [cs.SE], 2026

    work page internal anchor Pith review Pith/arXiv arXiv 2026

  48. [48]

    Automated feedback generation for competition-level code,

    J. Zhang, D. Li, J. C. Kolesar, H. Shi, and R. Piskac, “Automated feedback generation for competition-level code,” inProceedings of the 37th IEEE/ACM International Conference on Automated Software Engineering, ser. ASE 2022. ACM, 2022, pp. 13:1–13:13

    work page 2022

  49. [49]

    PyDex: Repairing bugs in introductory python assignments using LLMs,

    J. Zhang, J. P. Cambronero, S. Gulwani, V . Le, R. Piskac, G. Soares, and G. Verbruggen, “PyDex: Repairing bugs in introductory python assignments using LLMs,”Proceedings of the ACM on Programming Languages, vol. 8, no. OOPSLA1, pp. 1100–1124, 2024

    work page 2024

  50. [50]

    A systematic study of time limit exceeded errors in online programming assignments,

    J. Zhang, J. Gu, W. Zhang, J. P. Cambronero, J. C. Kolesar, R. Piskac, D. Li, and H. Shi, “A systematic study of time limit exceeded errors in online programming assignments,” arXiv:2510.14339 [cs.SE], 2025

    work page arXiv 2025

  51. [51]

    Using pre-trained language models to resolve textual and semantic merge conflicts,

    J. Zhang, T. Mytkowicz, M. Kaufman, R. Piskac, and S. K. Lahiri, “Using pre-trained language models to resolve textual and semantic merge conflicts,” inProceedings of the 31st ACM SIGSOFT Interna- tional Symposium on Software Testing and Analysis, ser. ISSTA 2022. ACM, 2022, pp. 77–88

    work page 2022

  52. [52]

    Learning CI configuration correctness for early build feedback,

    M. Santolucito, J. Zhang, E. Zhai, J. Cito, and R. Piskac, “Learning CI configuration correctness for early build feedback,” inProceedings of the 2022 IEEE International Conference on Software Analysis, Evolution and Reengineering, ser. SANER 2022. IEEE, 2022, pp. 1006–1017

    work page 2022

  53. [53]

    Static detection of silent misconfigurations with deep interaction analysis,

    J. Zhang, R. Piskac, E. Zhai, and T. Xu, “Static detection of silent misconfigurations with deep interaction analysis,”Proceedings of the ACM on Programming Languages, vol. 5, no. OOPSLA, pp. 1–30, 2021

    work page 2021

  54. [54]

    The state of the art in end-user software engineering,

    A. J. Ko, R. Abraham, L. Beckwith, A. Blackwell, M. Burnett, M. Erwig, C. Scaffidi, J. Lawrance, H. Lieberman, B. Myers, M. B. Rosson, G. Rothermel, M. Shaw, and S. Wiedenbeck, “The state of the art in end-user software engineering,”ACM Computing Surveys, vol. 43, no. 3, pp. 21:1–21:44, 2011

    work page 2011

  55. [55]

    Denali: A goal-directed superop- timizer,

    R. Joshi, G. Nelson, and K. Randall, “Denali: A goal-directed superop- timizer,” inProc. ACM SIGPLAN Conf. Programming Language Design and Implementation (PLDI), 2002, pp. 304–314

    work page 2002

  56. [56]

    Automatic generation of peephole superop- timizers,

    S. Bansal and A. Aiken, “Automatic generation of peephole superop- timizers,” inProc. Int. Conf. Architectural Support for Programming Languages and Operating Systems (ASPLOS), 2006, pp. 394–403

    work page 2006

  57. [57]

    Stochastic superoptimization,

    E. Schkufza, R. Sharma, and A. Aiken, “Stochastic superoptimization,” inProc. Int. Conf. Architectural Support for Programming Languages and Operating Systems (ASPLOS), 2013, pp. 305–316

    work page 2013

  58. [58]

    Rewrite rule inference using equality saturation,

    C. Nandi, M. Willsey, A. Zhu, Y . R. Wang, B. Saiki, A. Anderson, A. Schulz, D. Grossman, and Z. Tatlock, “Rewrite rule inference using equality saturation,”Proc. ACM Program. Lang. (OOPSLA), vol. 5, pp. 1–28, 2021

    work page 2021

  59. [59]

    Separation logic: A logic for shared mutable data structures,

    J. C. Reynolds, “Separation logic: A logic for shared mutable data structures,” inProc. IEEE Symp. Logic in Computer Science (LICS), 2002, pp. 55–74

    work page 2002

  60. [60]

    Resources, concurrency, and local reasoning,

    P. W. O’Hearn, “Resources, concurrency, and local reasoning,”Theoret- ical Computer Science, vol. 375, no. 1–3, pp. 271–307, 2007

    work page 2007

  61. [61]

    A logical view of composition,

    M. Abadi and G. D. Plotkin, “A logical view of composition,”Theoret- ical Computer Science, vol. 114, no. 1, pp. 3–30, 1993

    work page 1993