1
ScratchLens: Lens-Parametric Behavioral Equivalence for Scratch Programs
arXiv:2606.15817v2 [cs.PL] 16 Jun 2026
Yuan Si and Jialu Zhang∗ University of Waterloo, Waterloo, Canada [email protected], [email protected]
Abstract—Two Scratch programs can be syntactically far apart through renamed variables, split scripts, extracted custom blocks, and reordered initialization, while preserving the same behavior. A one-block edit, such as replacing a blocking broadcast with an asynchronous one, can create divergences that surface only under specific schedules. Behavioral equivalence for such programs is central to automated feedback, grading support, and repair validation. Existing tree differencing is too strict, and single-run dynamic comparison is unsound for concurrent, random, and timing-dependent behavior. The key observation is that equivalence for Scratch programs is parametric in an observation lens. We present a taxonomy that organizes behavioral divergence by causal phenomenon and observing lens, and we build ScratchLens, an equivalence checker structured around that taxonomy. ScratchLens compiles projects into a causal intermediate representation of typed resources and semantic transactions. It canonicalizes alpha-renamings, guards, and procedure bodies; quotients same-trigger concurrency by Mazurkiewicz trace normal forms over a conservative independence relation; separates program order from races; and supports residual-frontier handling through SMT obligations and counterexample-guided execution on the instrumented Scratch VM. Every conclusive verdict carries explicit evidence: equivalence by a bijection and trace quotient, difference by a typed witness, and unresolved cases remain explicit unknowns. We evaluate ScratchLens on a fully automated, VM-witnessed mutation corpus built from real Scratch projects, with per-lens ground-truth labels and a deep-composition stratum that hides each defect under a stack of equivalence-preserving refactorings. Under strict scoring that counts abstention as error, ScratchLens decides all 444 validated pairs and makes 0/158 false-equivalence claims on witnessed-different pairs; structural, dynamic-only, and large-language-model baselines fail on the classes predicted by the taxonomy, ablations quantify the contribution of partialorder reduction and lens parametricity, and the ambiguousmutant study shows that targeted scenarios expose divergences that random testing misses.
I. I NTRODUCTION Scratch is a large, real software ecosystem for introductory programming. More than 140 million children have created over a billion projects in it [1]. At this scale, automated feedback, grading support, repair validation, and hint generation all face the same question: when should two student programs be treated as behaviorally equivalent? The question is hard because Scratch programs are small event-driven systems: sprites, clones, variables, lists, monitors, broadcasts, ask queues, pen and sound effects, and renderer-visible state run on a cooperative green-thread VM [2]. The same behavior Corresponding author: Jialu Zhang.
admits many syntactic realizations (renames, script splitting, procedures, additive-update rewrites), while a one-block edit can change behavior through scheduling, random tokens, or frame timing; dropping broadcast and wait, for example, removes a join edge whose absence may appear only when a receiver is slow. This setting makes Scratch a compact stress test for software engineering methods. The language and environment were designed for broad creative programming [3], [4], and repository studies show that learners solve similar tasks through diverse block structures, sprites, and control decompositions [5]. An equivalence checker used by graders, feedback systems, or repair validators needs to preserve that diversity. It should accept correct refactorings across solution styles and reject causal changes that alter what a learner, tutor, or grader can observe. Program comparison tools need to control false alarms on refactorings and false equivalence claims on real bugs. Tree differencing [6], [7] over-approximates syntax because script boundaries and block order are not semantic; single-run dynamic comparison under-approximates behavior because it samples one schedule, random stream, and input trace [8]. In the debugging tutor that motivates ScratchLens, false equivalence is especially costly: it ends a learner’s debugging episode with the defect still present. Event-driven visual programs require lens-parametric equivalence. A glide and a jump can agree on final state and disagree on frames; two initialization scripts can agree under one schedule and diverge under another. The observer is part of the claim: final state, frame trace, monitors, stage output, event causality, or debug trace. We proceed in three steps. First, we define equivalence under an explicit lens and a taxonomy linking causal mechanisms (state, event causality, scheduling, randomness, time, clones, queues, persistent output), observation lenses, and typed root causes (Section III). The same vocabulary drives verdicts, mutation operators, and per-lens labels. Second, we build ScratchLens around that taxonomy (Sections IV–VI). Projects compile to CSIR: typed resources, footprints (reads, writes, consumes, spawns, joins, kills), and transactions cut at scheduler and lens-visible boundaries. Comparison combines rename-invariant canonicalization (usage profiles, one Weisfeiler–Leman refinement, bounded bijection search, expression and procedure normal forms, control-region paths, dead-branch pruning) with a Mazurkiewicz trace normal form [9] over a conservative independence relation. Residual
2
mismatches become typed causal differences, SMT side conditions, and targeted CEGAR scenarios for unresolved frontiers on an instrumented Scratch VM [10], [11]. The invariant is simple: every input that can influence lens-visible behavior is compiled and compared. Third, we evaluate with mechanical labels (Section VIII): equivalence labels come from correct-by-construction transforms plus VM falsification, difference labels require concrete VM witnesses, and mutants that the random validation battery leaves unresolved form an explicit ambiguous bucket. Baselines span structural, opcode-abstraction, dynamic-only, and LLM judges. We make the following contributions. • A two-axis taxonomy of behavioral divergence in Scratch programs, relating causal phenomena, observation lenses, and typed root causes (Section III). • Lens-parametric equivalence over CSIR, a causal intermediate representation whose transactions carry typed footprints, scheduler cuts, and provenance (Sections IV, V). • A comparison algorithm that combines rename-invariant canonicalization, trace normal forms with race structure, typed root-cause classification, bounded bijection fallback for tied profiles and explanations, and residual-frontier mechanisms based on SMT side conditions and VMbacked CEGAR (Section VI). • A reproducible, fully automated evaluation methodology for semantic equivalence checkers: a VM-witnessed mutation corpus over real projects with per-lens labels and a deep-composition stratum that separates semantic reasoning from textual difference-spotting, released as a benchmark together with operator manifests and generation scripts (Section VIII). • An implementation and evaluation under strict scoring against structural, dynamic, and LLM baselines, with ablations for partial-order reduction and lens collapse. II. RUNNING E XAMPLE Figure 1 distills the comparison problem that recurs throughout the paper. Program A is a reference game fragment: a bowl initializes score and lives, asks the apple to reset, and increments score when the bowl touches the apple. The apple reset handler hides the sprite, moves it to a random top-row position, and shows it again. A ≡ B: normalized refactoring. Program B keeps the join broadcast new-round
and wait
sender resumes after reset
B ̸≡ C: missing join edge. Program C deletes it
broadcast new-round sender may race reset
and rewrites change score by 1 as an assignment. A tree differencer sees many edits. The programs are behaviorally equivalent: resources admit a bijection, the initialization scripts write disjoint variables and commute, the custom block has the same canonical body as the original receiver, and the additive update normalizes to the same transaction. Program C changes only one block and diverges from Program B. The nonblocking broadcast removes the join edge from receiver completion to sender continuation. If fruit reset takes a frame, or if the next collision arrives before the receiver finishes, the bowl can continue while the fruit still has its old state. Final score may coincide, while event causality, frame trace, or stage-visible behavior differs. The verdict names the observation lens: A versus B is accepted with an explicit bijection and trace quotient; B versus C is rejected under lenses that observe the missing join edge, with a M ISSING J OIN E DGE witness. The example also fixes the role of the main abstractions used below. Variables, sprites, and messages become typed CSIR resources; independent initialization writes commute only when footprints prove independence; and the removed wait is an event-causal fact whose visibility depends on the selected lens. III. A TAXONOMY OF B EHAVIORAL D IVERGENCE The taxonomy asks, for each behavioral divergence, what mechanism causes it, which lenses observe it, and which typed root cause a checker should report. We derived it from the VM’s semantic carriers (Section IV) and cross-checked it against LitterBox bug patterns [12], [13]. A. Axis 1: Observation Lenses A lens is a projection from concrete traces to observations. Table I lists the lenses ScratchLens supports. Ldefault is the union of frame-visible, stage-visible, monitor, and eventcausal observations; it corresponds to what an attentive user of the running project can perceive. Lenses form a partial order when one projection includes another’s observations. We use “stronger” only for comparable lenses; for incomparable projections, ScratchLens reports a verdict vector indexed by lens. TABLE I O BSERVATION LENSES . E ACH PRESERVES A SUBSET OF TRACE INFORMATION ; Ldefault COMBINES THE MIDDLE FOUR . Lens
Preserved observations
Lfinal Lframe Lstage Lmonitor Levent Ldebug
Final variables, lists, target state, clone count Frame-boundary visual snapshots, yield structure Sprite, backdrop, pen, speech, sound effects Monitor values, visibility Broadcast, join, ask, clone, stop causality Primitive-level VM trace
Fig. 1. Running example. A distant refactoring (A/B) is equivalent, while a one-block change (B/C) removes the broadcast join edge and becomes visible under event-causal and frame-observing lenses.
B. Axis 2: Causal Phenomena
Program B looks very different from Program A: it renames variables, sprites, and messages; splits initialization into two green-flag scripts; extracts the reset logic into a custom block;
We organize supported Scratch divergences into eight carrier families. Each row of Table II names the phenomenon, the weakest lens family under which it becomes observable, the typed root causes ScratchLens reports for it, and the semantic
3
carrier that CSIR must preserve. Operator manifests in the artifact map these rows to generated mutations (Section VIII-A). Three properties matter downstream. Root causes are typed by carrier resource, so M ISSING J OIN E DGE names a broadcast message and U NINITIALIZED R EAD names a variable. Lens floors make labels vectors: a P5 operator can be different under Ldefault and equivalent under Lfinal . Finally, each phenomenon maps to CSIR footprint facts, letting the classifier recover root causes without syntax patterns and letting perroot-cause results double as per-phenomenon coverage. Two cases illustrate the boundary: same-trigger scripts that both write one variable become a P3 race fact, and concurrent ask blocks can reorder the global FIFO prompt queue under P7. The taxonomy also acts as a soundness contract. Legal simplifications preserve the carrier and the weakest observing lens. Renaming a variable preserves P1 facts only if all reads, writes, and monitor references move together. Reordering two scripts is valid only when their footprints prove independence; when both scripts write the same resource, the comparison records a P3 race fact. Likewise, replacing a glide by a move is an equivalence under Lfinal and a difference under Lframe . The contract prevents a single binary verdict from hiding why two reasonable observers can disagree. IV. S EMANTIC M ODEL A. Concrete Configurations We model a Scratch project as a transition system over configurations C = (Σ, Θ, H, A, K, E, F, O), where Σ is the store and visual state; Θ the green-thread pool; H hats and pending events; A the ask queue and answer; K clone families; E environment and random tokens; F frame, time, and redraw state; and O observations. The model follows the VM implementation [2]. Four facts drive the IR and corpus: threads run cooperatively within frames; loops yield once per iteration, so bounded unrolling must preserve synthetic frame barriers under Lframe ; broadcasts use casefolded message identity and restart running receivers; and ask-and-wait serializes through one global FIFO question queue. B. Lens-Parametric Equivalence A lens L projects concrete traces to observations (Table I). Two projects are equivalent under L when every admissible environment, random, time, and input stream produces equal L-projected traces, modulo alpha-renaming, stuttering of Lunobservable transactions, reordering of independent sametrigger transactions, and permutation of indistinguishable clone families. The schedule quotient treats the relative order of distinct same-trigger scripts as nondeterministic and reports dependence on it as a race (Section VI). The quotient preserves each lens-visible cut. Stuttering erases only L-unobservable transactions; broadcast joins remain visible under Levent , redraw boundaries under Lframe , and monitor toggles under Lmonitor . The alpha-renaming component is typed as well: a stage variable, a sprite-local
variable, a list region, and a broadcast message live in different resource spaces with separate maps. The restrictions let the implementation use compact canonical products while retaining a direct connection to VM behavior. V. C AUSAL S CRATCH IR A. Typed Resources and Footprints CSIR types every semantic carrier: VAR, L IST, TARGETP ROP, M ONITOR, A SK Q UEUE, A NSWER, R ANDOM S TREAM, T IMER, B ROADCAST M ESSAGE, C LONE FAMILY, T HREAD S ET, F RAME B OUNDARY, P EN B UFFER, S OUND C HANNEL, E NV T OKEN, E XTERNAL. Resources carry scope (global, sprite-local, clone-local) and, for lists, a region (whole, length, index, suffix). A footprint records reads, writes, creates, deletes, ordered-token consumes, observes, spawns, joins, kills, frame barriers, and commutative effects such as additive variable updates. B. Transactions and Compilation A transaction is a maximal effect sequence between scheduler- or lens-visible cuts: hats, waits, ask-and-wait, broadcasts and joins, clone birth and death, stops, loop backedges, promise waits, frame boundaries, and monitor updates. The compiler enforces the invariant that every behaviorally relevant input is compiled: guards and reporter arguments carry read/token footprints; menus resolve to selections; inline variable references become reads; bounded literal loops unroll with one synthetic frame barrier per iteration; statically false branches are pruned; sound procedures are inlined and the rest compared by canonical content digest. Unsupported extensions compile to opaque external resources; they reduce decisiveness and produce unknowns when their effects matter. Each compiled transaction records its trigger, target family, lexical provenance, normalized primitive sequence, controlregion path, footprint, and L-visible observations. The product compared by the algorithm is the multiset of these facts after alpha canonicalization and trace normalization. Facts are intentionally redundant: a broadcast contributes a message resource, a spawn edge, a receiver set, and optionally a join edge. The redundancy makes root-cause classification local. Removing broadcast and wait, for instance, changes a join fact without requiring the classifier to reconstruct a dynamic happens-before graph from raw blocks. VI. C OMPARISON A LGORITHM Algorithm 1 summarizes the comparison kernel. Every accepting path carries a witness: equality of canonical products, an explicit alpha bijection, or equality of the Lfinal abstract transfer. Mismatches become typed root causes plus obligations; targeted VM scenarios exercise only residual frontiers, and unproved cases remain explicit unknowns. Obligations are closed side conditions with a status in {proved, refuted}. Open predicates are recorded as frontiers. The last conclusive branch is deliberately narrow: L ENS S UFFICIENT(D, U, L) holds only for footprint-backed root causes whose observability under L is independent of
4
TABLE II TAXONOMY OF BEHAVIORAL DIVERGENCE . “L ENS FLOOR ” IS THE WEAKEST LENS FAMILY THAT OBSERVES THE PHENOMENON ; COMPARABLE STRONGER LENSES INHERIT THE DIFFERENCE .
Phenomenon
Carrier
Lens floor
Typed root causes
P1 State transformation P2 Event causality
variables, lists, properties broadcasts, joins, stops, triggers
Lfinal Levent
P3 Schedule sensitivity P4 Randomness, environment P5 Time and frames
same-trigger thread order random stream, input tokens
Levent /Lfinal any
ValueChange; GuardChange; UninitializedRead Missing/ExtraJoinEdge; BroadcastEdgeRemoved; TriggerChange; Missing/ExtraKillEdge race-structure mismatch RandomStreamShift
yields, waits, glides, timer
Lframe
P6 Clone lifecycle P7 Interaction queues P8 Persistent output
clone families, clone-start hats ask FIFO, answer pen buffer, monitors, sound, looks
Levent /Lstage Levent Lstage /Lmonitor
Algorithm 1 ScratchLens lens-parametric product comparison Require: projects Pr , Ps ; lens L; optional VM budget B 1: Cr , Cs ← C OMPILE CSIR(Pr , Ps ) 2: Mr , Ms ← A LPHAC ANON(Cr , Cs ) ▷ usage profiles + WL 3: (Fr , Or ) ← P RODUCT F EATURES(Cr , L, Mr ) 4: (Fs , Os ) ← P RODUCT F EATURES(Cs , L, Ms ) 5: if Fr = Fs and C LOSED(Or ∪ Os ) then return E QUIVALENT with (Mr , Ms ) and certificates Or ∪ Os 6: else if Fr = Fs then return U NKNOWN with frontier O PEN(Or ∪ Os ) 7: end if 8: (Fs′ , π, δ, Oπ ) ← B OUNDED T IE S EARCH(Fr , Fs , Cs , Ms ) 9: if δ = 0 and C LOSED(Or ∪ Oπ ) then return E QUIVALENT with explicit bijection π 10: else if δ = 0 then return U NKNOWN with frontier O PEN(Or ∪ Oπ ) 11: end if 12: (Tr , Ts , Ot ) ← F INALT RANSFER(Cr , Cs , L) 13: if L = Lfinal and Tr = Ts and C LOSED(Ot ) then return E QUIVALENT UNDER Lfinal with certificates Ot 14: else if L = Lfinal and Tr = Ts then return U NKNOWN with frontier O PEN(Ot ) 15: end if 16: D ← C LASSIFY(Cr , Cs , Fr , Fs′ , L) ▷ typed root causes 17: U ← O BLIGATIONS(D) ▷ solver fragment or frontier 18: if B > 0 and U contains a conditional frontier then 19: S ← S CENARIOS(U ) 20: W ← RUN TARGETEDVM(Pr , Ps , S, B) 21: if W confirms divergence then 22: return D IFFERENT(W ) 23: end if 24: end if 25: if L ENS S UFFICIENT(D, U, L) then 26: return D IFFERENT(D, U ) 27: end if 28: return U NKNOWN with frontier U
unresolved predicates. Masked-comparison items, unsupported reporters, and any root cause whose observability depends on an open obligation remain in U until solver discharge or a VM witness supports a conclusive D IFFERENT verdict. A. Canonicalization ScratchLens canonicalizes both projects independently, then compares canonical feature multisets. Expression trees fold
ChangedFrameBoundary; FramePathChange; ChangedTimerCausality ChangedCloneMultiplicity; CloneInitChange AskQueueOrderChanged PenEffectChange; EffectRemoved/Added; MonitorVisibleOnly
constants, orient comparisons, sort commutative operands, simplify negations, and normalize change v by c with set v to v + c. Every primitive also carries a controlregion path: enclosing control opcodes, branch indices, and guard expressions. Thus if c {set a; set b} and if c {set a}; set b no longer flatten to the same product; the former tags both writes with if#b0[c], the latter only the write to a. Statically decided guards contribute no path element. Resources receive canonical indices per kind and scope, ordered by a rename-invariant usage profile refined by one Weisfeiler–Leman round over co-footprint neighborhoods [14]. If the base comparison fails, ScratchLens searches remaining bijections over profile-tied resources by coordinate descent and a bounded small-space sweep. An equalizing bijection is a sound equivalence witness; otherwise the best bijection only minimizes the explanation delta. Usage profiles use semantic roles. A variable written by a green-flag initialization, read by a guard, and shown as a monitor has a different profile from a variable written only inside a clone-start script. The WL refinement adds neighborhood context: two variables that both appear in arithmetic updates can still separate if one co-occurs with a broadcast join and the other with a renderer-visible motion effect. Remaining ties are common in small projects with symmetric sprites or duplicate counters; the bounded search closes those cases inside proof construction. PAlgorithm 2 gives the search. Coordinate descent costs i |Gi |!; the relevance filter skips groups absent from the residual delta, and the full cross-product appears only under the small-space budget. In the corpus every proven equivalence closes by direct canonical equality; the search mainly provides a bounded fallback and explanation minimizer. Procedures are keyed by defining sprite. Bodies are compared by content digest over alpha-canonicalized primitives in the same trace normal form as transaction clusters (Section VI-B). The digest triple–raw, guard-masked, and constantmasked–lets the classifier distinguish G UARD C HANGE and VALUE C HANGE inside procedures and keeps procedure mismatches typed. Digests reach a call-graph fixpoint, accepting renamed-identical procedures and rejecting same-named dif-
5
Algorithm 2 Bounded bijection search over profile-tied resources Require: canonical features Fr , Fs ; tie groups G1 , . . . , Gk 1: Fbest ← Fs ; πbest ← ∅; Obest ← ∅; δ ∗ ← |Fr ⊖ F Ps | 2: for i ← 1 to k do ▷ coordinate descent, cost |Gi |! i 3: if no canonical token of Gi occurs in Fr ⊖ Fbest then continue 4: end if 5: for permutation π of Gi , others fixed at πbest do 6: recompute features and certificates (Fπ , Oπ ); δ ← |Fr ⊖ Fπ | 7: if δ = 0 then return (Fπ , π, 0, Oπ ) 8: end if 9: if δ < δ ∗ then Fbest ← Fπ ; πbest ← π; Obest ← Oπ ; ∗ δ ←δ 10: end if 11: end for 12: end for Q 13: full cross-product sweep when |Gi |! ≤ 64, budget 1024 i ∗ 14: return (Fbest , πbest , δ , Obest ) ▷ minimal-delta bijection
Algorithm 3 Trace normal form for one trigger cluster Require: transactions T with footprints, program-order edges Ep , lens L 1: E ← Ep ; R ← ∅ 2: for all unordered pairs (ti , tj ) ∈ T do 3: if I NDEPENDENT(ti , tj , L) then 4: continue 5: end if 6: if ti and tj come from distinct same-trigger scripts then 7: R ← R ∪ {R ACE FACT(ti , tj )} 8: else 9: E ← E ∪ {P ROGRAM O RDER(ti , tj )} 10: end if 11: end for 12: N ← lexicographically least topological order of (T, E) 13: F ← E MIT FACTS(N, L) ∪ R 14: return (F, R)
ferent ones. B. Trace Normal Forms with Race Structure Within each trigger cluster, ScratchLens proves pairwise independence from typed footprints. Transactions are independent only when read/write conflicts are absent (modulo declared commutative effects), neither consumes ordered tokens, L-visible observations commute, and no spawn, join, kill, or frame barrier fixes order. Unproved pairs are dependent. Within one script, dependence becomes program order; across scripts it becomes a race fact. Each cluster maps to the lexicographically least linearization of this partial order, a Mazurkiewicz trace normal form [9], [15]: interleavings of the same trace match, ordered scripts never match races, and fully independent transactions compare as a multiset. For example, two green-flag scripts that both write score emit an unordered race fact. Merging them into one ordered script changes the product; renaming the variable preserves the race fact under the alpha map. Equivalence preserves scheduler commitments as well as effects. Algorithm 3 is the step that keeps commutation and races separate. Independence is checked on typed footprints,
ordered-token consumption, lens-visible observations, and lifecycle edges. A dependent pair inside one script becomes program order; a dependent pair across same-trigger scripts becomes an unordered race fact. The canonical product then contains both the least linearization and the race facts. The representation accepts script splitting and commuting initializers while preserving scheduler commitments that a learner or tutor can observe under Levent or Lframe . C. Verdicts, Classification, and Obligations Equal canonical products prove equivalence only when their side conditions are closed. Under Lfinal , an abstract transfer over the numeric, string, list, clone, and monitor domains provides a second sound acceptance path when products differ only by final-state-invisible structure and the transfer obligation is proved. Unequal products enter the typed classifier, which recovers the taxonomy’s root causes from canonical fact deltas: join and spawn facts for P2, trigger sets for trigger changes, dangling send sets for broken broadcast wiring, readbefore-write summaries for uninitialized reads, clone-trigger feature isolation for clone initialization, pen and observation totals for P8, and masked feature comparison for guard and literal changes (a pair whose features equalize when guards are masked differs exactly in its guards). Classified items carry confidence. Footprint-backed kinds are sound: a missing join fact is a fact about compiled structure, and no execution can retract it. Masked-comparison kinds are conditional: guardmasked equality isolates the change to guard text, and semantic equivalence of those guards is a satisfiability question. The item becomes an obligation and, when the solver fragment leaves it open, a CEGAR frontier with a synthesized scenario. Supported obligations, including guard feasibility, list abstraction equality, clone partition equality, and broadcast join equivalence, discharge through Z3 when available and through an exact finite fallback otherwise [10]. Discharged obligations become certificates; open obligations stay in the frontier and are excluded from equivalence and static D IFFERENT certificates. D. CEGAR with the Instrumented VM Conditional frontiers become targeted scenarios: a randomstream frontier yields a scenario with two distinguishable token prefixes whose constraints (ri ̸= rj , range bounds) the solver instantiates; an ask-order frontier yields distinguishable answers; a join frontier yields a receiver-stress run. The runner executes both projects under identical deterministic oracles, records primitive, event, clone, monitor, and renderer signals, aligns trace segments back to CSIR transactions, and confirms or refutes the frontier. Spurious evidence mutates an explicit refinement state (random taint to indexed tokens, clone families to partitions, final summaries to frame snapshots, renderer hashes to pixel regions) and re-enters comparison, in the counterexample-guided tradition [11]. Frontiers are structured records. Each record names the carrier, lens, trigger path, unresolved predicate, candidate scenario generator, and the observations that would close the case. A random frontier records token indices and value constraints; an
6
TABLE III V ERDICT PATHS AND GUARANTEES . Path
Guarantee
Known exclusions
Canonical product equality
Lens equivalence with closed side conditions, modulo alpha-renaming, POR, stuttering, and procedure digests Same guarantee after bounded bijection search with closed side conditions Final-state equivalence over stated abstract domains with proved transfer obligation Difference for the named lens-visible carrier when root cause is lens-sufficient Concrete counterexample trace No semantic claim
Opaque extensions; unsupported reporters
Tie-group bijection
Lfinal transfer Static causal fact
VM witness U NKNOWN
Search may abstain
No frame/event/stage guarantee Other lenses may agree No equivalence proof Incomplete by design
ask frontier records question order and answer substitutions; a renderer frontier records the region or target property that must diverge. The record structure lets the implementation cache negative runs, refine only the affected abstraction, and report U NKNOWN with enough context for a stronger scenario or human review. E. Soundness Boundary ScratchLens is intentionally asymmetric: finite VM runs prove difference, while equivalence requires an accepting static path. Table III summarizes the contract. The theorem scope is the supported Scratch-VM subset compiled to CSIR: core variables/lists, target properties, broadcasts and joins, greenthread yields, clones, ask queues, monitors, renderer-facing state, and the reporters covered by the expression normalizer. Opaque extensions, unsupported reporters, solver timeouts, and open frontiers yield U NKNOWN unless a concrete witness is found. F. End-to-End Verdict Paths The kernel has only a few accepting shapes, and those shapes cover the cases that make Scratch comparison difficult. Consider an alpha-renamed project whose initialization script is split into two green-flag scripts. CSIR compilation assigns the renamed variables the same usage profiles, the split creates two transactions under the same trigger, and the independence relation proves that their footprints commute. The trace normal form emits the same product facts on both sides: the equivalence witness is the alpha map plus the trace quotient. Block-level similarity has no role in this proof path. For a missing broadcast and wait, compilation emits the same message resource and receiver-spawn facts and omits the join fact from receiver completion to sender continuation. The missing fact is a P2 mismatch, so the classifier reports M ISSING J OIN E DGE and names the message and receiver family. If the downstream observation is immediate, the static root cause is enough; if the difference requires receiver contention, the obligation synthesizes a receiver-stress scenario. A confirmed VM trace is a concrete witness; an unconfirmed scenario leaves the pair conditional.
For a glide replaced by a jump, the products differ in frame-path facts and renderer-visible target positions under Ldefault or Lframe . The same pair can still be accepted under Lfinal if the abstract transfer proves equal final coordinates, size, direction, variables, lists, and clone counts. The example shows why the verdict carries a lens: a single global label would either miss a visible frame difference or incorrectly reject a valid final-state equivalence. For guard and literal changes, the classifier first asks which masked product equalizes the pair. If guard-masked products match and raw products differ, the residual obligation is semantic guard equivalence. Simple numeric and string fragments discharge through the solver or finite fallback. If the guard lies outside the supported fragment, the frontier records the unknown expression and the transaction it controls; targeted execution may find a witness, and the static checker keeps the claim conditional until then. VII. I MPLEMENTATION ScratchLens comprises a Python analysis kernel and a Node.js VM harness. The kernel implements CSIR compilation, canonicalization, trace normal forms, classification, obligations, and refinement. The harness wraps scratch-vm v5.0.300 (repository SHA e6f5711) [2] with deterministic random, time, keyboard, broadcast, and ask oracles, recording tick snapshots plus primitive, event, clone, monitor, renderer, and collision signals; without headless GL it falls back to bounding boxes while preserving non-pixel traces. The kernel decides nothing by VM execution: VM runs provide witnesses and refutations only. The implementation passes 189 unit and soundness-regression tests covering the hardening fixes found during corpus development, including guard capture, menu resolution, loop-yield unrolling, sprite-scoped procedures, control-region paths, masked procedure digests, race structure, and tie search. The review artifact releases a runnable core subset: CSIR compilation, normalizers, canonical product comparison, trace normal forms, the static verdict driver for the controlled suite and non-LLM baselines, the VM trace harness, and aggregation scripts. It excludes private tutor integration, service deployment code, and credentials. The same harness validates labels, dynamic baselines, and targeted frontier scenarios, so oracle regressions produce quarantine spikes before labels can shift silently. Several regressions came directly from corpus development: inline-reference decoding, boundary-aware canonicalization of bare names, procedurebody normal forms, and coordinate-descent tie search were all hardened after generated pairs exposed a failure mode. VIII. E VALUATION The evaluation is designed to run without a human in the loop: every label is either correct by construction or witnessed by VM execution, abstention is a first-class outcome for every method, and false equivalence is the headline error. It asks six research questions. RQ1 How accurately does ScratchLens classify equivalent and different pairs on the labeled corpus, and how often does it abstain?
7
RQ2 When pairs differ, does ScratchLens recover the injected root cause? RQ3 How does ScratchLens compare with structural, abstraction, dynamic-only, and LLM baselines, in accuracy and in false-equivalence count? RQ4 On mutants left unresolved by a random scenario battery, how often do targeted scenarios expose the divergence? RQ5 What do partial-order reduction and lens parametricity contribute, and do per-lens verdicts match perlens labels? RQ6 What does the pipeline cost, and how often does each escalation layer decide? A. Corpus Construction Seeds are real Scratch projects that parse, compile, and execute headlessly, deduplicated by opcode multiset and stratified by size. Of 94 scanned projects, 60 are accepted (8 too small, 26 above the block cap), spanning 5–600 blocks; 44 use broadcasts, 18 clones, 17 randomness, 6 ask-andwait, and 4 extension blocks. Each seed yields identity pairs, semantics-preserving transforms, lens-differential transforms, and behavior-changing mutants instantiating Table II; some different mutants are further wrapped in benign refactoring noise. Operators mutate only code reachable from real event hats. The operator families are paired to the taxonomy. Equivalence operators rename variables and messages, split independent scripts, insert statically dead branches outside loop bodies, extract procedures, and rewrite additive updates. Lensdifferential operators preserve final state while changing an observable path, for example replacing a glide with a jump, inserting a wait, or changing loop-yield structure. Different operators remove or add joins, stops, triggers, guards, parameters, clone creation, message wiring, or observable effects. This design gives each admitted different pair both a semantic label and an injected root cause, while keeping equivalence pairs rich enough to defeat textual comparison. Labels are mechanical. Equivalent-labeled pairs face a deterministic falsification battery whose stimuli are translated through the recorded identifier bijection and whose observations are translated back; a renamed message is the same logical broadcast on both sides. Reproducible divergences quarantine the pair, while isolated Lfinal failures downgrade only that lens claim. Different-labeled pairs require a concrete VM witness; unwitnessed mutants enter the ambiguous bucket for RQ4. Labeling, dynamic-baseline, and ScratchLens CEGAR seeds are disjoint. The shipped corpus has 544 generated pairs: 444 headline pairs, 88 ambiguous pairs, and 12 quarantined pairs (2.2%). The quarantine history found computed-message renames, loop-body dead branches, reporter deletions, and two oracle-stimulus defects; each became a precondition or regression. The battery spans green-flag smoke runs, per-key taps and sweeps, sprite and stage clicks, broadcast injections and bursts, ask-and-answer scripts, and random-stream fuzzing under deterministic seeds. A pair whose full trace diverges is quarantined only when the divergence reproduces under the
TABLE IV C ORPUS COMPOSITION BY OPERATOR : PAIRS GENERATED AND PAIRS ADMITTED TO THE HEADLINE METRICS AFTER VALIDATION . D IFFERENT- LABELED PAIRS NEED A VM WITNESS , SO RARE - SCHEDULE OPERATORS HAVE LOWER ADMISSION RATES .
Operator
Class
Gen.
Usable
identity eq_alpha eq_dead_branch eq_msg_rename eq_add_xform eq_commute ld_wait_add / glide / unroll df_event_swap df_block_del df_stop_add df_join_add / drop df_param df_msg_break df_cond_flip df_clone_dup / init_del hard eq (4–6 EQ ops) hard df (1 DF + 3–5 EQ)
control EQ EQ EQ EQ EQ lens-diff DF DF DF DF DF DF DF DF composed composed
60 37 35 26 15 5 34 25 25 20 21 18 16 16 11 120 60
60 36 34 24 15 5 18 14 12 17 10 12 6 12 6 112 51
544
444
Total
same seed, filtering borderline-tick flakes. This validation policy is asymmetric by construction: equivalence-labeled pairs survive unless falsified, and different-labeled pairs require a positive witness. Admission is asymmetric: equivalence pairs survive VM falsification, and different pairs require positive witnesses. Rare-schedule operators populate the ambiguous bucket. The composed stratum stacks four to six equivalence transforms, or hides one bug under three to five such transforms, separating semantic reasoning from textual matching. The stratum models the tutoring case in which a learner both refactors and introduces one defect: the textual diff is large, and the semantic difference should remain a single root cause. Rendered-text judges get a shortcut on single edits; composition removes it. B. Methods Under Comparison ScratchLens runs in four configurations: full (static kernel with CEGAR), static-only, without partial-order reduction, and under Lfinal only. Static-only reports the kernel verdict before frontier escalation; on the headline corpus it coincides with full ScratchLens because no headline verdict requires escalation. The non-LLM baselines represent three method families: canonical fingerprint equality and normalized treeedit distance (structural); opcode multiset and ordered opcode traces (abstraction); and dynamic-only comparison, which runs N =5 deterministic scenarios and declares equivalence when no divergence appears. The dynamic baseline compares traces under the same identifier-translated quotient oracle as label validation, so its errors reflect genuine sampling brittleness, with identifier artifacts removed by the shared quotient. The LLM tier evaluates GLM-5.1, Qwen3.6-plus, and Kimi K2.6 through one OpenAI-compatible gateway, with served model identifiers, prompts, raw responses, and parsed JSON pinned in the artifact. Each model sees scratchblocks text, the Ldefault definition, and the closed taxonomy, then
8
returns strict JSON with verdict, optional root cause, and confidence; U NKNOWN is available, and persistent malformation counts as abstention. Requests use per-pair on-disk checkpoints and a single retry for malformed JSON, preventing transient gateway failures from re-judging decided pairs. The models do not see labels, VM witnesses, ScratchLens verdicts, or another model’s output. All methods see the same pairs and no labels, witnesses, or other outputs. Strict overall accuracy counts abstention as wrong; decided accuracy and coverage separate selectivity. Diagnosis requires both verdict and injected root cause. We also report different-class precision/recall, false equivalent/different counts, bootstrap 95% intervals, McNemar tests, and singleedit versus deep-composition strata [16], [17]. Strict scoring matches deployment. A selective judge that returns U NKNOWN on hard equivalences has no basis for suppressing false alarms as a tutor gate. We report both the selective and deployment views, and we isolate false equivalence because that error certifies a defective program as correct. False differences remain undesirable; in the motivating workflow they produce recoverable hints or review requests. C. Experimental Environment Experiments run on one 16-core Windows workstation. The VM stages perform about 19,000 deterministic scratch-vm executions; the LLM tier issues about 1,900 checkpointed gateway requests, under $10 total. The artifact records raw per-pair outputs, seeds, scenarios, and model responses before aggregation. The non-LLM matrix can be regenerated from the shipped corpus without network access; the LLM tables can be re-scored from pinned raw responses even if served model versions drift. D. RQ1–RQ2: Effectiveness Table VI reports 444 validated pairs. ScratchLens decides every pair with accuracy 1.000, different-class precision/recall 1.000/1.000, and 0 false equivalences, at a 0.22s median. The false-equivalence count is 0/158 on the validated different class; by the rule of three, the corresponding upper 95% empirical rate is about 1.9% on this corpus. Diagnosis reaches 0.987: 156 of 158 different pairs recover both verdict and root cause (Table V). The two misses are conservative C HANGED S E MANTIC B EHAVIOR fallbacks on deleted initializations masked by another write; deep-composition diagnosis is 51/51. Both misses share one abstraction: the read-before-write summary is order-insensitive, so deleting an initialization from one script is masked when another script writes the same variable. They are generic fallbacks with correct verdicts. The composed stratum causes no additional diagnostic loss because canonicalization strips the transform stack before classification. E. RQ3: Baseline Comparison Every family fails in its predicted direction. Structural comparison avoids false equivalence and rejects refactorings (182 false differences). Opcode abstractions accept mutants with unchanged opcode statistics (17–43 false equivalences).
TABLE V D IAGNOSIS BY INJECTED ROOT CAUSE : PAIRS WHOSE VERDICT AND ROOT CAUSE ARE BOTH RECOVERED , OVER ALL VALIDATED DIFFERENT- LABELED PAIRS .
Injected root cause
Pairs
Recovered
TriggerChange ExtraKillEdge ValueChange EffectRemoved GuardChange ExtraJoinEdge FramePathChange BroadcastEdgeRemoved ChangedFrameBoundary ChangedCloneMultiplicity UninitializedRead MissingJoinEdge
25 26 22 18 16 15 11 7 7 5 4 2
25 26 22 18 16 15 11 7 7 5 2 2
Total
158
156
TABLE VI V ERDICT QUALITY ON THE MUTATION CORPUS UNDER STRICT SCORING . OVERALL ACCURACY COUNTS AN ABSTENTION AS AN ERROR ; ACC @ DEC AND C OVERAGE GIVE THE ABSTENTION - AWARE DECOMPOSITION . FALSE E Q COUNTS DIFFERENT- LABELED PAIRS CLASSIFIED AS EQUIVALENT, THE FAILURE MODE THAT CERTIFIES DEFECTIVE PROGRAMS . D IAGNOSIS REQUIRES THE VERDICT AND THE INJECTED ROOT CAUSE TOGETHER ; METHODS THAT EMIT NO ROOT CAUSES SHOW –.
Method ScratchLens static kernel without POR Lfinal only Fingerprint equality Opcode multiset Opcode trace Tree distance Dynamic (N =5) GLM-5.1 Qwen3.6-plus Kimi K2.6
Overall
Acc@dec
Cov.
FEq
Diag.
1.000 1.000 0.955 0.721 0.579 0.597 0.608 0.590 0.899 0.928 0.849 0.977
1.000 1.000 0.955 0.721 0.579 0.597 0.608 0.590 0.899 0.969 0.959 0.982
1.000 1.000 1.000 1.000 1.000 1.000 1.000 1.000 1.000 0.957 0.885 0.995
0 0 0 124 17 19 43 0 28 9 15 8
0.987 0.987 0.987 – – – – – – 0.816 0.532 0.899
Dynamic testing reaches 0.899 overall, certifies 28 defective programs, and costs two orders of magnitude more time. LLMs form a coverage–soundness frontier: Kimi K2.6 is strongest (0.977 overall, 0.995 coverage) with 8 false equivalences; GLM-5.1 and Qwen3.6-plus also commit false equivalences and trail ScratchLens on diagnosis. McNemar tests reject every baseline and ablation at p < 0.01. Abstention is directional: GLM-5.1 abstains on 17 equivalent pairs against 2 different ones, and Qwen3.6-plus on 38 against 13. The models often point at a difference; the missing capability is exhaustive equivalence certification. Across all eleven comparisons, every pair on which ScratchLens and another method disagreed in correctness was decided correctly by ScratchLens. Table VII isolates deep composition, where one defect hides among benign refactorings. Structural comparison collapses from 0.751 to 0.313; dynamic testing concentrates 14 false equivalences there. Kimi K2.6 and GLM-5.1 hold accuracy better than Qwen3.6-plus, and all three still certify defective programs. ScratchLens remains 1.000 because canonicaliza-
9
TABLE VII OVERALL ACCURACY BY STRATUM ( ABSTENTION COUNTS AS ERROR ), AND FALSE EQUIVALENCES ON THE DEEP - COMPOSITION STRATUM ALONE . Method ScratchLens Tree distance Dynamic (N =5) GLM-5.1 Qwen3.6-plus Kimi K2.6
Single-edit
Composed
FEq (comp.)
1.000 0.751 – 0.915 0.904 0.975
1.000 0.313 0.871 0.951 0.755 0.982
0 – 14 5 7 1
tion removes the transform stack before classification. F. RQ4: Targeted Scenarios on the Ambiguous Bucket The ambiguous bucket contains 88 mutants left unresolved by random scenarios, concentrated in untriggered effects, weak join contention, frame timing, and receiver fallout. The static kernel records typed conditional frontiers for 88 of them; targeted scenarios confirm 14 concrete divergences (rate 0.159), usually on the first synthesized scenario, including position, costume, visibility, and clone-count witnesses. The dynamic baseline certifies eleven of these fourteen as equivalent. The unexposed remainder mixes genuinely equivalent mutants and divergences below the current oracle surface, so conditional frontiers remain conditional. The exposed witnesses use fresh seeds disjoint from both the labeling battery and the dynamic baseline. Three of the fourteen come from trigger-directed scenarios that press the keys named in the typed diff. The remaining 74 bucket members include trigger changes with no observable effect, join edits whose receivers finish too quickly to contend, broken broadcasts without sampled fallout, and value or guard edits below the current oracle signal.
TABLE VIII D ECISION - PATH PROFILE . H EADLINE COUNTS ARE CONCLUSIVE CORPUS VERDICTS ; FRONTIER COUNTS ARE CONDITIONAL RECORDS IN THE AMBIGUOUS BUCKET; CONTROLLED COUNTS ARE CONCLUSIVE OUTCOMES IN THE 26- CASE SEMANTIC SUITE . Path
Headline Frontier Controlled
Canonical equality Tie-group bijection Lfinal transfer Static root-cause fact Targeted VM witness U NKNOWN/frontier
286 0 0 0 0 0 158 88 cond. 0 14 0 74
7 0 1 18 0 0
tie-group acceptance. Different-labeled pairs close by static root-cause evidence; residual obligations appear in the ambiguous bucket, while the controlled suite exercises the Lfinal transfer path (Table VIII). The tail (5.0s p90, 27s p99) comes from minimal-delta explanations on composed differences. The dynamic baseline spends 29s median and still has 28 false equivalences; ScratchLens reserves VM cost for label validation and RQ4 frontiers. LLM latency is provider-bound at 4–10s. I. Controlled Phenomenon Coverage Independent of the mutation corpus, a hand-constructed suite of 26 minimal pairs covers each taxonomy phenomenon and the main static acceptance paths: 7 canonical equivalences, 1 Lfinal transfer, and 18 static-difference verdicts. ScratchLens decides all of them correctly with root-cause accuracy 1.000. VM-witness cases appear in the frontier bucket; the controlled suite counts conclusive static outcomes. Renderer and realproject smoke runs serve as implementation validations outside the effectiveness claims. IX. D ISCUSSION
G. RQ5: Ablations and the Lens Matrix Both ablations fail as predicted. Removing POR (0.955 overall), all twenty errors are false differences on commuted independent writes. The Lfinal -only configuration (0.721) keeps 1.000 precision and drops recall to 0.215 because 124 event-, frame-, and effect-level divergences are invisible to final state. On all 243 pairs with explicit Lfinal labels, Lfinal verdicts match the label vector, showing that each verdict is tied to its observer. A glide-for-jump pair illustrates the point: its label vector is ⟨Ldefault : D IFF, Lfinal : E Q⟩. The full kernel reports F RAME PATH C HANGE under Ldefault , while the Lfinal configuration proves equivalence through final-state transfer. A single-bit checker has no observer field to express both verdicts. H. RQ6: Cost and Escalation Profile The static kernel decides the validated corpus without VM execution at a 0.22s median. All 286 equivalences close by direct canonical equality; no headline equivalence relies on finite execution, Lfinal transfer, SMT discharge, or bounded
Oracle transport. Execution-based equivalence needs a transported oracle: stimuli translate forward through an identifier bijection and observations translate back. Two development failures, broadcast case normalization and renamedmessage stimuli, came from violating this rule. Ambiguity and deployment. The 88 ambiguous members mix genuine equivalents, unobserved divergences, and longerhorizon behaviors. RQ4 keeps them as typed frontiers until targeted scenarios expose 14 concrete divergences. In tutoring, U NKNOWN routes to review, while false equivalence ends debugging incorrectly. Strict scoring and explicit unknowns match the deployment contract. The static kernel handles interactive cases at a 0.22s median; unknowns route to dynamic evidence or human review. Artifact boundary. The public review path exposes the semantic checker through a fixed interface: CSIR export, canonical comparison, controlled-suite drivers, manifest-based ScratchLens reruns, trace replay, and aggregation. The private tutor service supplies deployment glue, credentials, and UI integration. Those components do not affect the verdict relation or the reported corpus metrics. This boundary lets reviewers rerun the analysis layer without gaining access to production infrastructure.
10
X. T HREATS TO VALIDITY
XII. C ONCLUSION
Construct and internal validity. We treat the reference VM as the operational semantics for Scratch 3 behavior in this study, but instrumentation can still be wrong. The harness records concrete execution only, never calls the static checker for labels, and uses disjoint seed namespaces. Generator/classifier coupling remains possible because operators share the taxonomy; prior bug patterns, deep-composition pairs, VM witness admission, and quarantine reduce this risk. Selection, external, and LLM validity. Witness admission under-represents rare-schedule and long-horizon bugs; 0/158 FEq is a corpus-specific empirical result. The corpus is Scratch 3 from one crawl source; other block languages need new carriers, cuts, and lenses. Public seeds may appear in LLM training data and served models drift, so the artifact pins model ids, prompts, raw responses, and parsed JSON. The 600-block cap removes projects whose traces are dominated by assets, long loops, or renderer effects; it keeps corpus generation reproducible and interactive, while under-sampling very large games and animation-heavy projects. The excluded 26 seeds are recorded in the manifest audit trail, so future corpora can raise the cap and measure whether clone-, timer-, and rendererheavy programs change the frontier mix.
Behavioral equivalence for event-driven block programs is lens-parametric. ScratchLens implements that contract with CSIR, trace normal forms over typed footprints, rename-invariant canonicalization, content-addressed procedures, typed witnesses, unknown frontiers, and VM-backed refinement. On 444 validated pairs, including 158 VM-witnessed differences, it makes 0/158 false-equivalence claims and recovers root causes with 0.987 accuracy. The broader lesson is methodological: learner-program equivalence needs an explicit observer, a transported test oracle, strict scoring, and a place for unknowns. Future work widens the frontier with wall-clock virtualization, monitor/audio oracles, procedure summaries, renderer witnesses, and front ends for other block languages.
XI. R ELATED W ORK Scratch analysis and testing. Hairball [18], Dr. Scratch [19], LitterBox [12], [13], Bastet [20], Whisker-style testing [8], [21], [22], NuzzleBug [23], and test-based hinting [24] analyze or guide one program. ScratchLens compares two programs and ties each root cause to a carrier and observation lens. Recent Scratch feedback systems [25], [26], repair work [27], and multimodal benchmarks [28], [29] use LLMs, gameplay videos, and execution evidence to surface semantic bugs that block structure alone can miss. ScratchLens targets the complementary equivalence problem needed to compare learner programs, reference solutions, and candidate repairs. Differencing and concurrency. Prior differencing and equivalence tools [6], [7], [30]–[37] target syntax or sequential programs; Scratch adds hats, cooperative scheduling, broadcasts, ask queues, clones, and renderer-visible state. The trace quotient builds on Mazurkiewicz theory [9] and partial-order reduction [15], [38], [39]; CEGAR [11] handles frontiers, and lenses make the observer explicit [40]. Work on semantic merge conflicts and feedback generation for conventional code also compares related program versions or candidate repairs, but targets textual languages and judge-style traces rather than event-driven Scratch lenses [41], [42]. Mutation methodology and artifacts. The evaluation adapts mutation analysis [43], [44] to a setting where equivalent mutants are expected, useful, and lens-dependent. Traditional mutation studies often discard equivalent mutants as noise [45]; we keep unresolved cases as an ambiguous bucket, attach typed frontiers, and separate random validation from targeted exposure. The released manifests preserve the operator chain, seed identity, checksums, VM scenarios, verdicts, and aggregation inputs, making the benchmark auditable even when a reviewer chooses to rerun only a controlled suite or sample.
11
R EFERENCES [1] Scratch Foundation, “Scratch 2024: Creativity around the world,” https: //annualreport.scratchfoundation.org/, 2025, accessed 2026-06-14. [2] ——, “scratch-vm v5.0.300: Virtual machine used to represent, run, and maintain the state of programs for scratch 3.0,” https://github.com/scratchfoundation/scratch-vm, 2026, repository SHA e6f5711f25f607ce8370a5a7afcfb391b349a6e1; repository archived 2026-06-10 and migrated to scratch-editor; accessed 2026-06-12. [3] M. Resnick, J. Maloney, A. Monroy-Hernández, 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. [4] 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. [5] E. Aivaloglou and F. Hermans, “How kids code and how we know: An exploratory study on the scratch repository,” in Proceedings of the 2016 ACM Conference on International Computing Education Research, ser. ICER ’16. ACM, 2016, pp. 53–61. [6] J.-R. Falleri, F. Morandat, X. Blanc, M. Martinez, and M. Monperrus, “Fine-grained and accurate source code differencing,” in Proceedings of the 29th ACM/IEEE International Conference on Automated Software Engineering, ser. ASE ’14. ACM, 2014, pp. 313–324. [7] K. Zhang and D. Shasha, “Simple fast algorithms for the editing distance between trees and related problems,” SIAM Journal on Computing, vol. 18, no. 6, pp. 1245–1262, 1989. [8] A. Stahlbauer, M. Kreis, and G. Fraser, “Testing scratch programs automatically,” in Proceedings of the 27th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ser. ESEC/FSE ’19. ACM, 2019, pp. 165–175. [9] A. Mazurkiewicz, “Trace theory,” in Petri Nets: Applications and Relationships to Other Models of Concurrency. Springer, 1987, pp. 278–324. [10] L. de Moura and N. Bjørner, “Z3: An efficient SMT solver,” in Tools and Algorithms for the Construction and Analysis of Systems, ser. TACAS ’08. Springer, 2008, pp. 337–340. [11] E. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith, “Counterexampleguided abstraction refinement for symbolic model checking,” Journal of the ACM, vol. 50, no. 5, pp. 752–794, 2003. [12] G. Fraser, U. Heuer, N. Körber, F. Obermüller, and E. Wasmeier, “LitterBox: A linter for scratch programs,” in Proceedings of the 43rd IEEE/ACM International Conference on Software Engineering: Software Engineering Education and Training, ser. ICSE-SEET ’21. IEEE, 2021, pp. 183–188. [13] C. Frädrich, F. Obermüller, N. Körber, U. Heuer, and G. Fraser, “Common bugs in scratch programs,” in Proceedings of the 2020 ACM Conference on Innovation and Technology in Computer Science Education, ser. ITiCSE ’20. ACM, 2020, pp. 89–95. [14] B. Weisfeiler and A. Leman, “A reduction of a graph to a canonical form and an algebra arising during this reduction,” Nauchno-Technicheskaya Informatsia, vol. 2, no. 9, pp. 12–16, 1968. [15] P. Godefroid, Partial-Order Methods for the Verification of Concurrent Systems, ser. Lecture Notes in Computer Science. Springer, 1996, vol. 1032. [16] Q. McNemar, “Note on the sampling error of the difference between correlated proportions or percentages,” Psychometrika, vol. 12, no. 2, pp. 153–157, 1947. [17] B. Efron and R. J. Tibshirani, An Introduction to the Bootstrap. Chapman & Hall/CRC, 1994. [18] B. Boe, C. Hill, M. Len, G. Dreschler, P. Conrad, and D. Franklin, “Hairball: Lint-inspired static analysis of scratch projects,” in Proceeding of the 44th ACM Technical Symposium on Computer Science Education, ser. SIGCSE ’13. ACM, 2013, pp. 215–220. [19] J. Moreno-León, G. Robles, and M. Román-González, “Dr. scratch: Automatic analysis of scratch projects to assess and foster computational thinking,” RED. Revista de Educación a Distancia, no. 46, 2015. [20] A. Stahlbauer, C. Frädrich, and G. Fraser, “Verified from scratch: Program analysis for learners’ programs,” in Proceedings of the 35th IEEE/ACM International Conference on Automated Software Engineering, ser. ASE ’20. ACM, 2020, pp. 150–162. [21] A. Deiner, C. Frädrich, G. Fraser, S. Geserer, and N. Zantner, “Automated test generation for scratch programs,” Empirical Software Engineering, vol. 28, no. 3, p. 79, 2023.
[22] K. Götz, P. Feldmeier, and G. Fraser, “Model-based testing of scratch programs,” in Proceedings of the 2022 IEEE Conference on Software Testing, Verification and Validation, ser. ICST ’22. IEEE, 2022, pp. 411–421. [23] A. Deiner and G. Fraser, “NuzzleBug: Debugging block-based programs in scratch,” in Proceedings of the 46th IEEE/ACM International Conference on Software Engineering, ser. ICSE ’24. ACM, 2024, pp. 1–13. [24] F. Obermüller, E. Wasmeier, and G. Fraser, “Guiding next-step hint generation using automated tests,” in Proceedings of the 26th ACM Conference on Innovation and Technology in Computer Science Education, ser. ITiCSE ’21. ACM, 2021, pp. 220–226. [25] D. Li, D. Li, H. Shi, and J. Zhang, “Raven: Rethinking automated assessment for scratch programs via video-grounded evaluation,” 2026. [26] Y. Si, K. Qi, D. Li, H. Shi, and J. Zhang, “Stitch: Step-by-step LLM guided tutoring for scratch,” 2025. [27] Y. Si, M. Wang, D. Li, H. Shi, and J. Zhang, “EcoScratch: Cost-effective multimodal repair for scratch using execution feedback,” 2026. [28] Y. Si, D. Li, H. Shi, and J. Zhang, “ViScratch: Using large language models and gameplay videos for automated feedback in scratch,” 2025. [29] Y. Si, S. Han, D. Li, H. Shi, and J. Zhang, “ScratchEval: A multimodal evaluation framework for llms in block-based programming,” 2026. [30] B. Fluri, M. Würsch, M. Pinzger, and H. Gall, “Change distilling: Tree differencing for fine-grained source code change extraction,” IEEE Transactions on Software Engineering, vol. 33, no. 11, pp. 725–743, 2007. [31] D. Jackson and D. A. Ladd, “Semantic diff: A tool for summarizing the effects of modifications,” in Proceedings of the International Conference on Software Maintenance, ser. ICSM ’94. IEEE, 1994, pp. 243–252. [32] S. K. Lahiri, C. Hawblitzel, M. Kawaguchi, and H. Rebêlo, “SYMDIFF: A language-agnostic semantic diff tool for imperative programs,” in Computer Aided Verification, ser. CAV ’12. Springer, 2012, pp. 712– 717. [33] S. Person, M. B. Dwyer, S. Elbaum, and C. S. Păsăreanu, “Differential symbolic execution,” in Proceedings of the 16th ACM SIGSOFT International Symposium on Foundations of Software Engineering, ser. FSE ’08. ACM, 2008, pp. 226–237. [34] B. Godlin and O. Strichman, “Regression verification: Proving the equivalence of similar programs,” Software Testing, Verification and Reliability, vol. 23, no. 3, pp. 241–258, 2013. [35] D. A. Ramos and D. R. Engler, “Practical, low-effort equivalence verification of real code,” in Computer Aided Verification, ser. CAV ’11. Springer, 2011, pp. 669–685. [36] A. Pnueli, M. Siegel, and E. Singerman, “Translation validation,” in Tools and Algorithms for the Construction and Analysis of Systems, ser. TACAS ’98. Springer, 1998, pp. 151–166. [37] C. K. Roy, J. R. Cordy, and R. Koschke, “Comparison and evaluation of code clone detection techniques and tools: A qualitative approach,” Science of Computer Programming, vol. 74, no. 7, pp. 470–495, 2009. [38] C. Flanagan and P. Godefroid, “Dynamic partial-order reduction for model checking software,” in Proceedings of the 32nd ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, ser. POPL ’05. ACM, 2005, pp. 110–121. [39] A. Valmari, “The state explosion problem,” in Lectures on Petri Nets I: Basic Models. Springer, 1998, pp. 429–528. [40] R. Milner, Communication and Concurrency. Prentice Hall, 1989. [41] J. Zhang, T. Mytkowicz, M. Kaufman, R. Piskac, and S. K. Lahiri, “Using pre-trained language models to resolve textual and semantic merge conflicts (experience paper),” in Proceedings of the 31st ACM SIGSOFT International Symposium on Software Testing and Analysis, ser. ISSTA ’22. ACM, 2022, pp. 77–88. [42] J. Zhang, D. Li, J. C. Kolesar, H. Shi, and R. Piskac, “Automated feedback generation for competition-level code,” in Proceedings of the 37th IEEE/ACM International Conference on Automated Software Engineering, ser. ASE ’22. ACM, 2022. [43] R. A. DeMillo, R. J. Lipton, and F. G. Sayward, “Hints on test data selection: Help for the practicing programmer,” Computer, vol. 11, no. 4, pp. 34–41, 1978. [44] Y. Jia and M. Harman, “An analysis and survey of the development of mutation testing,” IEEE Transactions on Software Engineering, vol. 37, no. 5, pp. 649–678, 2011. [45] D. Schuler and A. Zeller, “Covering and uncovering equivalent mutants,” Software Testing, Verification and Reliability, vol. 23, no. 5, pp. 353– 374, 2013.