The reviewed record of science sign in
Pith

arxiv: 2607.00635 · v1 · pith:AJV32LMS · submitted 2026-07-01 · cs.SE

Checked Program Recovery from Execution Video: A Sound Oracle for Untrusted Generators

Yuan Si , Jialu Zhang This is my paper

Reviewed by Pith T0 review T1 audit T2 compute T3 formal T4 kernel 2026-07-02 08:42 UTCgrok-4.3pith:AJV32LMSrecord.jsonopen to challenge →

classification cs.SE
keywords program recoveryexecution videoScratchvalidation oraclelens equivalencestatic checkeruntrusted generatorconcurrency quotient
0
0 comments X

The pith

A two-tier oracle with a static checker certifies Scratch program recovery from execution video without accepting incorrect programs.

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

The paper develops a trustworthy way to recover runnable Scratch programs from videos of their execution even when the generator proposing candidates is untrusted. It centers on a two-tier validation oracle whose static checker proves lens-equivalence to a reference program and issues a certificate that never accepts a wrong program, while the renderer component can only refute or show finite agreement. Tested on 246 labeled differing pairs including adversarial cases designed to trap the concurrency model, the oracle makes no false accepts; outside its vocabulary and on real projects it abstains or refutes without ever accepting an incorrect program. In-vocabulary recoveries match their sources frame for frame and most earn certificates, while real projects recover at a 14 percent rate that stays vocabulary-bound and error-free. A frontier vision-language model recovers none single-shot, and oracle-guided repair lifts it only modestly, showing the gap a sound checker creates for untrusted generators.

Core claim

The paper introduces a two-tier validation oracle for recovering Scratch programs from execution video. A static checker proves lens-equivalence using a partial-order independence quotient to model concurrency and issues certificates that, under the assumption the quotient is adequate, never accept an incorrect program. A renderer can only refute or witness finite agreement. On 246 labeled differing pairs, including an adversarial battery targeting the concurrency quotient, the oracle makes no false accepts; on inputs outside the vocabulary and on real projects it abstains or refutes, accepting none tested. In-vocabulary recoveries reproduce their source frame for frame and 80 percent earn a

What carries the argument

The two-tier validation oracle, in which a static checker proves lens-equivalence via the partial-order independence quotient and issues certificates while a renderer only refutes or witnesses agreement.

If this is right

  • In-vocabulary recoveries reproduce their source frame for frame.
  • 80 percent of in-vocabulary recoveries earn a static certificate.
  • Whole real projects recover at a 14 percent rate that remains vocabulary-bound and never inflates with a wrong answer.
  • A frontier vision-language model recovers none of the matched programs single-shot while the structured pipeline with the oracle recovers all.

Where Pith is reading between the lines

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

  • The oracle design could be tested on program recovery tasks that use other visual or sensor-based observations beyond Scratch video.
  • The deliberate asymmetry between the certifying checker and the refuting renderer might generalize to other synthesis settings where generators lack guarantees.
  • Extending the vocabulary or refining the quotient could raise recovery rates on real projects while preserving the no-false-accept property.

Load-bearing premise

The partial-order independence quotient adequately models concurrency in Scratch programs so the static checker can prove lens-equivalence without accepting an incorrect program.

What would settle it

A pair of programs that differ in behavior visible in the video yet receive a certificate from the static checker, or a real Scratch program whose concurrency behavior escapes the partial-order independence quotient.

Figures

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

Figure 1
Figure 1. Figure 1: From program to video and back. Perception and synthesis propose [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: The recoverability frontier. The fraction of a corpus a lens conflates [PITH_FULL_IMAGE:figures/full_fig_p004_2.png] view at source ↗
read the original abstract

A growing class of tools recovers a program from observations of its behavior using an untrusted generator, a neural model or a search, that proposes candidates with no correctness guarantee. We study how to make such recovery trustworthy, in the concrete setting of recovering a runnable Scratch program from a recording of its execution. The recording shows what the program does but never its code; many programs produce the same video, so the source cannot be recovered, and the right target is a program that behaves the same as far as the camera can tell, made precise with a lens. The core is a two-tier validation oracle with a deliberate verdict asymmetry. A static checker proves lens-equivalence to a reference and issues a certificate that, granting the partial-order independence quotient adequate, never accepts a wrong program; a renderer can only refute or witness finite agreement, never certify. Around it, Vid2Prog reads each sprite's motion, visibility, and timing from the video and a known-asset manifest and synthesizes a candidate source-free; a closed loop renders and runs recovery again for ground truth. Under the exact lens the oracle makes no false accept on 246 labeled differing pairs, including an adversarial battery built to trap its concurrency quotient; on inputs outside the vocabulary and on real projects it abstains or refutes, accepting none we test. In-vocabulary recoveries reproduce their source frame for frame and 80% earn a static certificate, while whole real projects, mostly outside the vocabulary, recover at 14%, a vocabulary-bound rate the system never inflates with a wrong answer. A frontier vision-language model recovers none of the matched programs single-shot, which oracle-in-the-loop repair lifts only to a few while the structured pipeline recovers all, the gap a sound checker makes for an untrusted generator.

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 / 2 minor

Summary. The paper presents Vid2Prog, a pipeline that recovers runnable Scratch programs from execution videos using an untrusted generator (neural or search-based). Recovery is validated by a two-tier oracle: a static checker that proves lens-equivalence to a reference program via a partial-order independence quotient for concurrency and issues a certificate (granting the quotient adequate, never accepting a wrong program), paired with a renderer that can only refute or witness finite agreement. The system reads sprite motion/visibility/timing from video plus an asset manifest; a closed re-execution loop provides ground truth. Under the exact lens the oracle reports zero false accepts on 246 labeled differing pairs (including an adversarial battery targeting the concurrency quotient); in-vocabulary recoveries reproduce frame-for-frame with 80% earning certificates, while real projects (mostly out-of-vocabulary) recover at 14% with no erroneous accepts; a frontier VLM recovers none single-shot.

Significance. If the partial-order independence quotient adequately models Scratch concurrency, the work supplies a sound, deliberately asymmetric oracle for certifying outputs of untrusted program generators from observational data. The explicit adversarial testing, closed-loop validation, and abstention behavior on out-of-vocabulary inputs are concrete strengths that distinguish it from purely empirical or self-referential checkers.

major comments (1)
  1. [two-tier oracle description] Description of the two-tier oracle and certificate issuance: the central soundness claim that the static checker 'never accepts a wrong program' (granting the quotient adequate) is load-bearing on the modeling assumption that the partial-order independence quotient captures all relevant concurrency behaviors of Scratch. The reported adversarial battery on 246 pairs provides empirical support but remains a domain-specific validation rather than a completeness argument or machine-checked proof for the language primitives; the manuscript should either supply additional justification (e.g., enumeration of concurrency primitives and why the quotient is complete for them) or explicitly bound the class of programs for which the claim holds.
minor comments (2)
  1. [abstract] The abstract states results on 'real projects' and 'in-vocabulary' recoveries but does not define the vocabulary boundary or the criteria used to classify a program as in- or out-of-vocabulary; a short clarifying sentence would improve readability.
  2. [Vid2Prog pipeline] Figure captions and the description of the closed re-execution loop should explicitly note that the renderer component can never issue a positive certificate, to avoid any reader confusion with the static checker's role.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the detailed and constructive feedback on the two-tier oracle. We address the major comment below.

read point-by-point responses

  1. Referee: Description of the two-tier oracle and certificate issuance: the central soundness claim that the static checker 'never accepts a wrong program' (granting the quotient adequate) is load-bearing on the modeling assumption that the partial-order independence quotient captures all relevant concurrency behaviors of Scratch. The reported adversarial battery on 246 pairs provides empirical support but remains a domain-specific validation rather than a completeness argument or machine-checked proof for the language primitives; the manuscript should either supply additional justification (e.g., enumeration of concurrency primitives and why the quotient is complete for them) or explicitly bound the class of programs for which the claim holds.

    Authors: We agree that the central soundness claim is conditional on the adequacy of the partial-order independence quotient, as already signaled by the qualifier 'granting the quotient adequate' throughout the manuscript. The adversarial battery on 246 pairs (including targeted concurrency traps) supplies strong empirical evidence of zero false accepts but does not constitute a formal completeness argument or machine-checked proof. In the revised version we will (1) enumerate the concurrency primitives covered by our vocabulary (event dispatch, broadcast-and-wait, sprite cloning, timer and variable updates under the event-driven model) and (2) supply a short justification, grounded in Scratch's published semantics, for why the quotient preserves the observable independence relations among these primitives. We will also add an explicit bounding statement that the 'never accepts a wrong program' guarantee applies only to programs whose behavior is fully expressible within the supported vocabulary and primitives. These changes directly respond to the request while preserving the conditional nature of the claim. revision: yes

Circularity Check

0 steps flagged

No significant circularity; soundness claim is conditional on an explicit external assumption

full rationale

The paper's central soundness statement is explicitly conditional ('granting the partial-order independence quotient adequate, never accepts a wrong program') and is supported by independent empirical validation on 246 labeled pairs, an adversarial battery, ground-truth rendering loops, and re-execution. No derivation step reduces by construction to a fitted parameter, self-definition, or self-citation chain; the adequacy of the quotient is treated as a domain modeling assumption rather than proven inside the paper, and the oracle's no-false-accept result on tested cases is reported as an empirical outcome, not a tautology.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 1 invented entities

The central claim depends on the domain assumption that the partial-order independence quotient adequately captures Scratch concurrency for lens-equivalence proofs, plus the definition of the lens as the observable equivalence target; no free parameters or new invented entities with independent evidence are introduced.

axioms (1)
  • domain assumption The partial-order independence quotient is adequate to model concurrency in Scratch programs for lens-equivalence checking.
    Invoked when describing how the static checker issues certificates without false accepts.
invented entities (1)
  • lens no independent evidence
    purpose: Precise definition of observable behavioral equivalence from video recordings.
    Introduced to specify the recovery target; no independent evidence outside the paper is provided.

pith-pipeline@v0.9.1-grok · 5854 in / 1505 out tokens · 34465 ms · 2026-07-02T08:42:53.556523+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

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

  1. [1]

    ScratchLens: Lens-Parametric Behavioral Equivalence for Scratch Programs

    Y . Si and J. Zhang, “ScratchLens: Lens-parametric behavioral equivalence for Scratch programs,” 2026, arXiv:2606.15817 [cs.PL]

    work page internal anchor Pith review Pith/arXiv arXiv 2026

  2. [2]

    Trace theory,

    A. W. Mazurkiewicz, “Trace theory,”Advances in Petri Nets, LNCS 255, pp. 279–324, 1987

    work page 1987

  3. [3]

    Dynamic partial-order reduction for model checking software,

    C. Flanagan and P. Godefroid, “Dynamic partial-order reduction for model checking software,” inProc. 32nd ACM SIGPLAN-SIGACT Symp. Principles of Programming Languages (POPL), 2005, pp. 110–121

    work page 2005

  4. [4]

    The hungarian method for the assignment problem,

    H. W. Kuhn, “The hungarian method for the assignment problem,”Naval Research Logistics Quarterly, vol. 2, no. 1-2, pp. 83–97, 1955

    work page 1955

  5. [5]

    Simple online and realtime tracking,

    A. Bewley, Z. Ge, L. Ott, F. Ramos, and B. Upcroft, “Simple online and realtime tracking,” inIEEE Int. Conf. Image Processing (ICIP), 2016, pp. 3464–3468

    work page 2016

  6. [6]

    Active learning literature survey,

    B. Settles, “Active learning literature survey,” University of Wisconsin- Madison, Tech. Rep. Computer Sciences Technical Report 1648, 2009

    work page 2009

  7. [7]

    Learning regular sets from queries and counterexamples,

    D. Angluin, “Learning regular sets from queries and counterexamples,” Information and Computation, vol. 75, no. 2, pp. 87–106, 1987

    work page 1987

  8. [8]

    Probable inference, the law of succession, and statistical inference,

    E. B. Wilson, “Probable inference, the law of succession, and statistical inference,”Journal of the American Statistical Association, vol. 22, no. 158, pp. 209–212, 1927

    work page 1927

  9. [9]

    Automating string processing in spreadsheets using input- output examples,

    S. Gulwani, “Automating string processing in spreadsheets using input- output examples,” inProc. 38th ACM SIGPLAN-SIGACT Symp. Princi- ples of Programming Languages (POPL), 2011, pp. 317–330

    work page 2011

  10. [10]

    Program synthesis by sketching,

    A. Solar-Lezama, “Program synthesis by sketching,” Ph.D. dissertation, University of California, Berkeley, 2008

    work page 2008

  11. [11]

    Program synthesis,

    S. Gulwani, O. Polozov, and R. Singh, “Program synthesis,”Foundations and Trends in Programming Languages, vol. 4, no. 1-2, pp. 1–119, 2017

    work page 2017

  12. [12]

    Syntax-guided synthesis,

    R. Alur, R. Bod ´ık, G. Juniwal, M. M. K. Martin, M. Raghothaman, S. A. Seshia, R. Singh, A. Solar-Lezama, E. Torlak, and A. Udupa, “Syntax-guided synthesis,” inFormal Methods in Computer-Aided Design (FMCAD), 2013, pp. 1–8

    work page 2013

  13. [13]

    Synthesizing data structure transformations from input-output examples,

    J. K. Feser, S. Chaudhuri, and I. Dillig, “Synthesizing data structure transformations from input-output examples,” inProc. ACM SIGPLAN Conf. Programming Language Design and Implementation (PLDI), 2015, pp. 229–239

    work page 2015

  14. [14]

    FlashMeta: A framework for inductive program synthesis,

    O. Polozov and S. Gulwani, “FlashMeta: A framework for inductive program synthesis,” inProc. ACM SIGPLAN Int. Conf. Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), 2015, pp. 107–126

    work page 2015

  15. [15]

    DeepCoder: Learning to write programs,

    M. Balog, A. L. Gaunt, M. Brockschmidt, S. Nowozin, and D. Tarlow, “DeepCoder: Learning to write programs,” inInt. Conf. Learning Representations (ICLR), 2017

    work page 2017

  16. [16]

    RobustFill: Neural program learning under noisy i/o,

    J. Devlin, J. Uesato, S. Bhupatiraju, R. Singh, A. rahman Mohamed, and P. Kohli, “RobustFill: Neural program learning under noisy i/o,” inInt. Conf. Machine Learning (ICML), 2017, pp. 990–998

    work page 2017

  17. [17]

    DreamCoder: Bootstrapping inductive program synthesis with wake-sleep library learning,

    K. Ellis, C. Wong, M. I. Nye, M. Sabl ´e-Meyer, L. Morales, L. B. Hewitt, L. Cary, A. Solar-Lezama, and J. B. Tenenbaum, “DreamCoder: Bootstrapping inductive program synthesis with wake-sleep library learning,” inProc. 42nd ACM SIGPLAN Conf. Programming Language Design and Implementation (PLDI), 2021, pp. 835–850

    work page 2021

  18. [18]

    Cypher, Ed.,Watch What I Do: Programming by Demonstration

    A. Cypher, Ed.,Watch What I Do: Programming by Demonstration. MIT Press, 1993

    work page 1993

  19. [19]

    Lieberman, Ed.,Your Wish is My Command: Programming by Example

    H. Lieberman, Ed.,Your Wish is My Command: Programming by Example. Morgan Kaufmann, 2001

    work page 2001

  20. [20]

    Program- ming by demonstration using version space algebra,

    T. A. Lau, S. A. Wolfman, P. M. Domingos, and D. S. Weld, “Program- ming by demonstration using version space algebra,”Machine Learning, vol. 53, no. 1-2, pp. 111–156, 2003

    work page 2003

  21. [21]

    Neural program synthesis from diverse demonstration videos,

    S.-H. Sun, H. Noh, S. Somasundaram, and J. J. Lim, “Neural program synthesis from diverse demonstration videos,” inInt. Conf. Machine Learning (ICML), 2018, pp. 4790–4799

    work page 2018

  22. [22]

    Leveraging grammar and reinforcement learning for neural program synthesis,

    R. Bunel, M. J. Hausknecht, J. Devlin, R. Singh, and P. Kohli, “Leveraging grammar and reinforcement learning for neural program synthesis,” in Int. Conf. Learning Representations (ICLR), 2018

    work page 2018

  23. [23]

    Execution-guided neural program synthesis,

    X. Chen, C. Liu, and D. Song, “Execution-guided neural program synthesis,” inInt. Conf. Learning Representations (ICLR), 2019

    work page 2019

  24. [24]

    Deep convolutional inverse graphics network,

    T. D. Kulkarni, W. F. Whitney, P. Kohli, and J. B. Tenenbaum, “Deep convolutional inverse graphics network,” inAdvances in Neural Information Processing Systems (NeurIPS), 2015, pp. 2539–2547

    work page 2015

  25. [25]

    Approximate bayesian image interpretation using generative probabilistic graphics programs,

    V . K. Mansinghka, T. D. Kulkarni, Y . N. Perov, and J. B. Tenenbaum, “Approximate bayesian image interpretation using generative probabilistic graphics programs,” inAdvances in Neural Information Processing Systems (NeurIPS), 2013, pp. 1520–1528

    work page 2013

  26. [26]

    Neural scene de-rendering,

    J. Wu, J. B. Tenenbaum, and P. Kohli, “Neural scene de-rendering,” in IEEE Conf. Computer Vision and Pattern Recognition (CVPR), 2017, pp. 7035–7043

    work page 2017

  27. [27]

    Neural- symbolic VQA: Disentangling reasoning from vision and language understanding,

    K. Yi, J. Wu, C. Gan, A. Torralba, P. Kohli, and J. B. Tenenbaum, “Neural- symbolic VQA: Disentangling reasoning from vision and language understanding,” inAdvances in Neural Information Processing Systems (NeurIPS), 2018, pp. 1039–1050

    work page 2018

  28. [28]

    Learning to infer graphics programs from hand-drawn images,

    K. Ellis, D. Ritchie, A. Solar-Lezama, and J. B. Tenenbaum, “Learning to infer graphics programs from hand-drawn images,” inAdvances in Neural Information Processing Systems (NeurIPS), 2018, pp. 6062–6071

    work page 2018

  29. [29]

    Learning to infer and execute 3d shape programs,

    Y . Tian, A. Luo, X. Sun, K. Ellis, W. T. Freeman, J. B. Tenenbaum, and J. Wu, “Learning to infer and execute 3d shape programs,” inInt. Conf. Learning Representations (ICLR), 2019

    work page 2019

  30. [30]

    Native x86 decompilation using semantics-preserving structural analysis and iterative control-flow structuring,

    D. Brumley, J. Lee, E. J. Schwartz, and M. Woo, “Native x86 decompilation using semantics-preserving structural analysis and iterative control-flow structuring,” inProc. 22nd USENIX Security Symposium, 2013, pp. 353–368

    work page 2013

  31. [31]

    preserve functional- ity

    H. Tan, Q. Luo, J. Li, and Y . Zhang, “LLM4Decompile: Decompiling bi- nary code with large language models,”arXiv preprint arXiv:2403.05286, 2024

    work page arXiv 2024

  32. [32]

    Coda: An end-to-end neural program decompiler,

    C. Fu, H. Chen, H. Liu, X. Chen, Y . Tian, F. Koushanfar, and J. Zhao, “Coda: An end-to-end neural program decompiler,” inAdvances in Neural Information Processing Systems (NeurIPS), 2019, pp. 3703–3714

    work page 2019

  33. [33]

    DIRE: A neural approach to decompiled identifier naming,

    J. Lacomis, P. Yin, E. J. Schwartz, M. Allamanis, C. L. Goues, G. Neubig, and B. Vasilescu, “DIRE: A neural approach to decompiled identifier naming,” inProc. 34th IEEE/ACM Int. Conf. Automated Software Engineering (ASE), 2019, pp. 628–639

    work page 2019

  34. [34]

    Extracting code from programming tutorial videos,

    S. Yadid and E. Yahav, “Extracting code from programming tutorial videos,” inProc. ACM Int. Symp. New Ideas, New Paradigms, and Reflections on Programming and Software (Onward!), 2016, pp. 98–111

    work page 2016

  35. [35]

    Too long; didn’t watch! extracting relevant fragments from software development video tutorials,

    L. Ponzanelli, G. Bavota, A. Mocci, M. D. Penta, R. Oliveto, M. Hasan, B. Russo, S. Haiduc, and M. Lanza, “Too long; didn’t watch! extracting relevant fragments from software development video tutorials,” inProc. 38th Int. Conf. Software Engineering (ICSE), 2016, pp. 261–272

    work page 2016

  36. [36]

    psc2code: Denoising code extraction from programming screencasts,

    L. Bao, Z. Xing, X. Xia, D. Lo, M. Wu, and X. Yang, “psc2code: Denoising code extraction from programming screencasts,”ACM Trans. Software Engineering and Methodology, vol. 29, no. 3, pp. 21:1–21:38, 2020

    work page 2020

  37. [37]

    Dr. scratch: A web tool to automatically evaluate scratch projects,

    J. Moreno-Le ´on and G. Robles, “Dr. scratch: A web tool to automatically evaluate scratch projects,” inProc. Workshop in Primary and Secondary Computing Education (WiPSCE), 2015, pp. 132–133

    work page 2015

  38. [38]

    Testing scratch programs automatically,

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

    work page 2019

  39. [39]

    LitterBox: A linter for scratch programs,

    G. Fraser, U. Heuer, N. K ¨orber, F. Oberm ¨uller, and E. Wasmeier, “LitterBox: A linter for scratch programs,” inProc. 43rd Int. Conf. Software Engineering: Software Engineering Education and Training (ICSE-SEET), 2021, pp. 183–188

    work page 2021

  40. [40]

    Hairball: Lint-inspired static analysis of scratch projects,

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

    work page 2013

  41. [41]

    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. Int. Computing Education Research (ICER), 2016, pp. 53–61

    work page 2016

  42. [42]

    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

  43. [43]

    The scratch programming language and environment,

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

    work page 2010

  44. [44]

    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

  45. [45]

    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

  46. [46]

    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

  47. [47]

    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

  48. [48]

    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

  49. [49]

    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

  50. [50]

    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

  51. [51]

    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

  52. [52]

    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

  53. [53]

    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 International Symposium on Software Testing and Analysis, ser. ISSTA 2022. ACM, 2022, pp. 77–88

    work page 2022

  54. [54]

    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

  55. [55]

    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

  56. [56]

    Translation validation,

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

    work page 1998

  57. [57]

    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

  58. [58]

    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. 42nd ACM SIGPLAN Conf. Programming Language Design and Implementation (PLDI), 2021, pp. 65–79

    work page 2021

  59. [59]

    Data-driven equivalence checking,

    R. Sharma, E. Schkufza, B. R. Churchill, and A. Aiken, “Data-driven equivalence checking,” inProc. ACM SIGPLAN Int. Conf. Object- Oriented Programming, Systems, Languages, and Applications (OOP- SLA), 2013, pp. 391–406

    work page 2013

  60. [60]

    Semantic program alignment for equivalence checking,

    B. R. Churchill, O. Padon, R. Sharma, and A. Aiken, “Semantic program alignment for equivalence checking,” inProc. 40th ACM SIGPLAN Conf. Programming Language Design and Implementation (PLDI), 2019, pp. 1027–1040

    work page 2019

  61. [61]

    Proof-carrying code,

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

    work page 1997

  62. [62]

    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

  63. [63]

    Automatic patch generation by learning correct code,

    F. Long and M. C. Rinard, “Automatic patch generation by learning correct code,” inProc. 43rd ACM SIGPLAN-SIGACT Symp. Principles of Programming Languages (POPL), 2016, pp. 298–312

    work page 2016

  64. [64]

    Angelix: Scalable multiline program patch synthesis via symbolic analysis,

    S. Mechtaev, J. Yi, and A. Roychoudhury, “Angelix: Scalable multiline program patch synthesis via symbolic analysis,” inProc. 38th Int. Conf. Software Engineering (ICSE), 2016, pp. 691–701

    work page 2016