SchedCheck: Schedule-Robustness Analysis for Event-Driven Block Programs

SchedCheck: Schedule-Robustness Analysis for Event-Driven Block Programs Yuan Si and Jialu Zhang∗

arXiv:2607.00623v1 [cs.SE] 1 Jul 2026

University of Waterloo, Waterloo, Canada [email protected], [email protected]

Abstract—Block-based languages such as Scratch let beginners assemble interactive programs from sprites and scripts. These programs are concurrent in practice: green-flag scripts, broadcasts, and clones run as cooperatively scheduled threads over shared sprite and stage state, and their authors never write a thread. We show that such programs contain schedule-sensitive behaviors whose observable result depends on an execution order the language leaves open. Editing, saving, or remixing a project can produce a copy with the same blocks but a different layer order, changing the order the virtual machine starts scripts. We formalize the schedule space a Scratch virtual machine can realize as the permutations of the initial executable-target order, and define schedule-robustness against a lattice of observation lenses over a fixed horizon. A partial-order exploration runs one schedule per dependence-equivalence class, and on projects small enough to enumerate, an independent oracle confirms it recovers every realizable outcome. On larger projects, representatives stand in for the factorial under the validated dependence model. SchedCheck implements this on the production Scratch VM. Across 224 real student projects, at least 21% of the concurrent ones are schedulesensitive at the grading lens, and a uniform random sample of public projects replicates the rate at 17.6%, with two real remixes of a deployed animation arranging its letters differently. On handbuilt fault pairs and a generated benchmark of 32 spec-defined faults across four classes, the tool detects and localizes every schedule fault, with a logic-fault control reporting clean. The oracle exposed four unsoundness gaps in the dependence model, all repaired. The method is parametric in the execution model, instantiating unchanged on a second cooperative event loop.

I. I NTRODUCTION Scratch is the entry point to programming for tens of millions of children. A learner drags blocks onto sprites, clicks the green flag, and watches a scene come alive. Underneath the friendly surface the runtime is concurrent. Every sprite can carry several scripts that start together on the green flag, react to broadcasts, or run inside clones, and all of them read and write shared state: variables, lists, and the position, costume, and visibility of every sprite. The learner writes interacting threads without ever naming one. Consider a child who builds a small game where a ball drops onto a paddle and a counter records the catch: the paddle checks whether it touches the ball and sets a variable, and the ball moves to the paddle. The child runs it, sees the catch register, and shares it. A classmate remixes the project, opening it and saving a copy, which carries the two sprites in a different layer order, and now the paddle sometimes checks for contact Corresponding author: Jialu Zhang.

before the ball has moved. Same blocks, same inputs, same random seed, yet the counter reads zero, and nothing in the project is a recognizable bug. The behavior depends on the order in which the two green-flag scripts start, and that order is not fixed by the language. This is a schedule-sensitive fault, and the schedule it depends on is realizable by a routine user action. A Scratch virtual machine starts green-flag scripts in a deterministic sweep over the sprites in layer order, so the relative order of two sprites’ scripts is exactly the relative order of the sprites on the stage. Reordering sprites is a one-click operation in the editor, and saved copies of a project can differ in it. A program whose result changes under such a reordering can carry a defect that single runs, fixed inputs, and code review all miss. Existing analyses for Scratch look elsewhere. Test generators such as Whisker [1] drive a project with synthesized inputs and check acceptance under one execution per input; static checkers such as LitterBox [2] flag bug patterns and code smells in the block graph. Both target correctness in the space of inputs or the shape of the code, and neither perturbs the schedule. Classical concurrency testing does [3], [4], yet it explores interleavings of a fixed or dynamically spawned thread set, a model that overshoots the single ordering choice a Scratch VM actually exposes. We take the schedule itself as the object of testing. The realizable schedule space of a Scratch program under a fixed input and seed is the set of runs obtained by permuting the initial inter-sprite order, a finite space the production VM can reproduce through a layer reordering. We define schedule-robustness of a program against an observation lens as agreement of the observed behavior across this space. The lens hierarchy, from the final state up to the full per-tick trace, is the one existing work uses to compare two Scratch programs [5]; we reuse it to ask whether one program agrees with itself across its schedules, so a verdict states what an order change can and cannot affect. A program is schedule-sensitive at a lens when two realizable orders disagree there, and the witness is two concrete runs. Exploring the space naively costs a factorial number of executions, and two algorithms make the exploration sound and legible. The first is a partial-order reduction over a typed dependence relation: orders that agree on every dependent pair are equivalent, the equivalence classes are the acyclic orientations of the conflict graph, and the explorer runs the VM

once per class, not k! times. The second explains a difference, keeping the observables an order moves, subtracting the order sensitivity a paired reference carries, and scoping what remains to the two scripts that contend for a resource. An independent oracle enumerates all orders on small projects and confirms the reduction recovers the same outcomes, a check that exposed four dependence gaps, two on the course corpus, one on the public sample, and one the broadcast and clone reduction surfaced, all of which we repaired.

Paddle (Sensor) when

clicked

touching Ball set caught

Ball (Mover) when

?

clicked

go to x: 0 y: 0

to yes

else set caught

to no

Fig. 1. The ball-and-paddle project. Under (Ball, Paddle) the ball moves before the test and caught becomes yes; under (Paddle, Ball) the test runs first and it becomes no. The orders differ only by sprite layout, which a remix changes.

SchedCheck realizes this design on the production Scratch VM. We evaluate it on 224 real student projects and a labeled benchmark, and we report seven findings. Schedule-sensitivity II. BACKGROUND is common: at least 21% of the concurrent projects change their final-state observable under some realizable order, and 25% A. The Scratch execution model change a finer observable; a uniform random sample of public A Scratch project [6], [7] is a set of targets, one stage and projects replicates this at 17.6%. The reduced exploration is a number of sprites. Each target owns scripts, and each script sound in practice, matching exhaustive enumeration with no begins with a hat block that names the event that starts it: missed outcome on all 142 course and 77 public projects the green flag, the receipt of a broadcast, or the creation of a an oracle could check, where it caught and we repaired four clone. A target also owns mutable state that other scripts can footprint gaps. On three hand-built admissible fault pairs the observe: local and global variables and lists, and the sprite’s tool detects and localizes all three, and stays silent on a live position, direction, costume, size, visibility, and graphic effects. logic fault that perturbs no schedule. Schedule perturbation Scripts that run at the same time share this state, which makes a reaches faults that input generation and static smell checkers project a concurrent program over shared memory even though leave untouched. A repaired program re-certifies as schedule- its author manipulates only blocks. robust while preserving its intended behavior. The method The runtime advances in ticks at thirty frames per second. is parametric in the execution model, its model-level parts Within a tick the virtual machine steps each active script until instantiating unchanged on a second cooperative event loop. the script yields, and a script yields at a loop boundary, a timed The orders it flags do occur between real saved copies: the wait, the join of a broadcast-and-wait, or a screen refresh. A remix family of a deployed logo animation assembles its letters forever loop runs one iteration per tick and lets every other in different places under two orders its copies save. Such script run in between. Execution is cooperative: a script holds manifestation is rare, though, and most sensitive projects stay the machine until it chooses to yield, and the machine never latently fragile. preempts it mid-step. Concurrency enters through three event sources. The green flag starts every green-flag script at once. A broadcast starts This paper makes the following contributions. It formalizes the scripts that listen for its message, and a broadcast-and-wait the realizable schedule space and schedule-robustness of an additionally holds the sender until those scripts finish. A clone event-driven block runtime, and proves that every schedule block copies a sprite and starts the copy’s clone-start scripts. the explorer reports is reproducible on the unmodified VM. It The three sources differ in when they create threads, yet they backs the exploration with an independent oracle: on every share the same shared state, so two scripts started by different project small enough to enumerate, the oracle runs all orders events can race on a variable or a sprite property exactly as and confirms the reduction misses no outcome, so the verdict two green-flag scripts can. The green flag is the common case there is checked exhaustively, and the partial-order reduction and the one a remix perturbs, and it anchors the model that carries the same model-based verdict to projects too large to follows; broadcasts and clones extend the same shared-state enumerate, one representative per dependence class. It gives picture. a set-valued, site-scoped attribution that reduces a scheduleFigure 1 shows the two scripts of the ball-and-paddle project. sensitive difference to the pair of scripts and the resource Reading them together makes the dependence visible: the behind it, avoiding the false negatives of a boolean divergence paddle’s touch test reads the ball’s position, and the ball’s check. It implements SchedCheck on the production Scratch move writes it, so the two scripts contend for the ball’s pose VM, quantifies schedule-sensitivity across a course corpus and and their order decides the test. a random sample of public projects, exhibits the perturbed order between real saved copies and measures how seldom B. The scheduler and its single degree of freedom remixing realizes it, measures detection and localization against The production VM keeps active scripts in an ordered list seeded faults and a static-analysis baseline, and reports the and, on every sub-tick pass, steps them in list order. The order implementation, benchmark design, and evaluation results. of this list at the start of a run is the only place where a choice

enters. When the green flag fires, the VM sweeps the targets in the VM appends in the same executable-target order; a clone’s layer order and appends each target’s green-flag scripts to the scripts start at a position its creator fixes, so two clones spawned list in block-storage order. The relative order of two sprites’ in one tick run in their creators’ layer order, which makes clone scripts in the list equals the relative order of those sprites on the scheduling a function of π and not a choice beyond it. Writing stage. Everything after this point is a deterministic function of execH (P, ι, r, π) for the H-tick run under initial order π, the the list and the program. Clones and freshly matched broadcast realizable schedule space is receivers append to the end of the list as they appear, and a Sched (P, ι, r, H) = { execH (P, ι, r, π) : π ∈ Sk }. restarted receiver keeps its position, so no later event reopens the ordering choice. The space is finite, and every element is a genuine run of This pins down what a perturbation may change. Layer the unmodified VM: assigning the sprites the layer order π order is editable: a user sends a sprite forward or backward, produces exactly this run. or remixes a project that was saved with a different layout, Theorem 1 (Realizability): For every π ∈ Sk there is and the green-flag sweep then produces a different starting list. a layer assignment under which the unmodified VM, on The within-target order of several scripts on one sprite is fixed the same P, ι, r, produces execH (P, ι, r, π). Consequently by block storage and is not separately editable. The realizable any behavioral difference SchedCheck reports between two freedom is the permutation of the initial inter-sprite order, and explored schedules is exhibited by two real runs that differ a sprite that the stage always renders at the back contributes only in sprite layer order. its scripts as a fixed suffix. The argument rests on how the VM starts scripts. On a We hold two further sources of variation fixed throughout. green-flag, broadcast, or input event, the VM matches hats by The pseudo-random generator is seeded, so a draw depends sweeping the executable targets in layer order [8] and appends only on the number of prior draws. The clock advances by a the matching threads in that order, so the relative order of fixed amount per tick, so a reader of the timer sees a value any two targets’ threads, at the first fan-out and at every later tied to the tick and not to how much work ran. These choices one, is the relative layer order of those targets. Assigning the isolate the schedule as the variable under study, and they supply sprites the layer order π therefore reproduces π at every such the determinism a tester needs to attribute a difference to the fan-out at once. Clone creation starts the new clone’s scripts order alone. at a position fixed by its creator, so two clones spawned in one tick run in the layer order of their creators, and clone III. S CHEDULES AND ROBUSTNESS scheduling is a function of π rather than a choice beyond it; This section fixes what a schedule is, which schedules a a broadcast-and-wait join records the receivers’ identities, not run can realize, and what it means for a program to be robust their list positions, so the reordering preserves it; and in-place against them. We write P for a project, ι for a fixed input and restart is a function of the run so far. Hence execH (P, ι, r, π) IO state, and r for a fixed seed. is a run of the unmodified VM on the layer-reordered project, by the deterministic sweep of Section II. A. The realizable schedule space Two consequences shape the rest of the paper. The space is A configuration is the ordered executable-target list, the the symmetric group Sk , not an unbounded tree of interleavings, per-target thread lists, the shared state, and the set of pending which is what makes a complete exploration tractable. The events. The shared state holds the variables and lists and, for stage is a fixed suffix, because it is rendered at the back and every sprite, its position, direction, costume, size, visibility, no layer change moves it past a sprite, so permuting it would and effects. A step runs one thread to its next yield, which describe a run the VM cannot produce. reads and writes a bounded set of resources and may append a thread for a clone or a receiver. A tick is a sequence of B. Observation lenses What counts as a difference depends on what an observer steps in list order until the threads quiesce, after which the watches. We reuse the observation lenses of existing work [5], clock advances and the observation is recorded. With the seed four that form a chain from coarse to fine. The final-state and clock pinned, a tick is a deterministic function of the lens reports the variables, lists, and sprite poses at the horizon. configuration, so a run over a fixed horizon of H ticks is a The frame-visible lens adds the per-tick rendered poses. The deterministic function of the program, the input, the seed, and monitors lens adds the on-stage variable and list watchers. The the initial executable-target order. full-trace lens adds the clone and event history. Each coarser The one free choice is the initial order of the executable observation is a projection of the next finer one, written targets, the layer order the VM sweeps when it starts scripts; Section II fixes everything else. Let π range over the perfinal ⊑ frame ⊑ monitors ⊑ full, mutations of the k contributing sprite targets, the executable sprite targets with a hat that can fire under the fixed input or so agreement at a finer lens forces agreement at every coarser is reachable from one through modeled broadcast and clone one. The lens is part of a verdict because it states the strength edges, the stage held fixed; including an inert target only adds of the claim: a difference at the full-trace lens may be invisible equivalent orders. The order π determines the green-flag thread to a player, while a difference at the final-state lens changes list, and equally the later broadcast and input fan-outs, which the result the project is built to produce.

Lemma 1 (Monotonicity): If two runs agree under a finer lens, they agree under every coarser lens. A program robust at a finer lens is robust at every coarser lens. The lemma follows from the projection structure: each coarser observation is a function of the next finer one, so equality of the finer observations carries to the coarser. The practical reading is a decay curve. As the lens coarsens from the full trace to the final state, the set of schedule-sensitive projects can only shrink, and the gap between the two ends measures fragility that an order change introduces during a run yet that the program resolves before it ends. C. Schedule-robustness

budget through this clock, so the number of script steps in a tick follows from the program and not from wall-clock time. It pins the project timer and the calendar reads that some sprites consult, which otherwise vary between runs. Advancing the clock per tick, not per read, keeps it from coupling to the interleaving while still letting timer-driven behavior progress. The harness guards every measurement with a determinism check. It runs the identity order twice and requires the two full traces to agree exactly. A project that fails this check has a residual source of nondeterminism that the harness does not pin, and SchedCheck marks it untrusted and leaves its differences unattributed. Across the corpus this check fails on no project, which gives confidence that a difference under reordering is a scheduling effect.

Definition 1 (Schedule-robustness): P is schedule-robust at lens L for (ι, r) over horizon H when all schedules in Sched (P, ι, r, H) agree under L. P is schedule-sensitive at L B. Witnesses when two of them disagree. A witness is two sprite orders and the observations they Robustness is monotone along the chain by Lemma 1, so a produce, and both run on the unmodified VM by Theorem 1. verdict targets the grading lens, the lens at which a project’s A bare witness names two outcomes without explaining them. intended result lives, and reports the coarser robustness for free. SchedCheck turns it into a cause: the conflict graph names the The ball-and-paddle project of Section I is schedule-sensitive at pair of scripts whose order the witness flips and the resource the final-state lens, since the counter variable takes two values they contend for, a write and a read of the same variable, a across the two sprite orders. A witness is the pair of orders broadcast whose receiver the sender no longer waits for, or a together with the values they produce, and the witness runs on sprite that reads another’s pose before that sprite has moved. the stock VM. On a labeled control-mutant pair the set-valued attribution of Schedule-robustness restates a classical idea for this setting. Section V sharpens this to the exact observables the fault makes A program robust at the full-trace lens is one whose realizable order-sensitive. The contended pair is the information a fix has schedules all produce the same run up to the reordering of to act on and the diagnosis a learner can read. independent work, which is the determinacy that Bernstein’s conditions characterize for two pieces of work [9] and that C. Fault classes Schedule-sensitive faults in Scratch recur in four shapes, Mazurkiewicz trace theory lifts to a set of events [10]. The lens lattice grades this notion: a program can be determinate and the names describe the contended resource. A missing at the level a grader observes while two of its schedules still broadcast-and-wait lets a sender continue before the receiver it differ in an order an instrument could record. A verdict carries triggered has finished, so a value the receiver was to prepare is both a yes-or-no answer and the lens at which it holds, and the read early; the contended resource is the variable the receiver next sections turn the definition into a procedure that decides writes. A read before initialization has one green-flag script read a variable that a second green-flag script initializes, and it and a reduction that decides it cheaply. the order of the two scripts decides whether the read sees the IV. T ESTING FOR S CHEDULE S ENSITIVITY initial value. A clone-initialization race uses a clone before SchedCheck tests a project by running it under several the clone’s own setup has run, so the clone is observed in a realizable schedules and comparing what it observes. The loop half-built state. A sensing race has a sprite test another sprite’s fixes the input and seed, chooses an initial sprite order, sets the position or contact before that sprite has moved, which is the green-flag thread list to that order, and runs the VM to a fixed shape of the ball-and-paddle project. The four classes share a horizon. It records the observation at each lens. A project is structure, a write and a read of one resource whose order the schedule-sensitive at a lens when two orders produce different language leaves open, and they organize the benchmark and the witnesses the tool reports. observations there, and the two orders form the witness. A. A determinism harness

D. Admissible faults for measurement

A reported difference is only meaningful when the order is the one thing that changed. The harness removes every other source of variation. It seeds the random generator so a draw is a function of the number of prior draws, and it gives identifier allocation its own seeded counter so clone and variable identities do not drift between runs and shift the values that depend on them. It freezes the clock to advance by one tick of simulated time per step and routes the sequencer’s work

To measure detection we need faults whose ground truth we control. A seeded fault pairs a control program with a mutant. The pair is an admissible schedule fault when three conditions hold. The mutant’s effect must be observable at some lens. The mutant must agree with the control under the identity order, so a fault that changes behavior under every order is a logic fault, not a schedule fault, and falls outside this measurement. The disagreement must appear under some realizable initial order,

which excludes a fault that only a sub-tick interleaving could expose. The control plays the role of the repaired program, and the gap between control and mutant under reordering is the fault we want a tool to find.

equivalent exactly when they orient every conflict edge the same way, that is, when for every dependent pair of sprites they agree on which sprite comes first. Lemma 2 (Class signature): Let the signature of an order be the orientation it gives to each conflict edge. Two orders V. E XPLORING AND E XPLAINING THE S CHEDULE S PACE are equivalent under independent adjacent swaps if and only The schedule space is finite, yet enumerating Sk costs k! if they have the same signature. The number of classes equals runs and most of those runs agree. This section gives the two the number of acyclic orientations of the conflict graph. The forward direction holds because an independent adjacent algorithms at the center of the approach. The first explores the space at one run per dependence-equivalence class, not swap exchanges two sprites that share no conflict edge, so no k! runs, and recovers every distinct observable outcome. The edge changes orientation and the signature is unchanged. The second takes a difference the first reports and reduces it to reverse direction sorts one order into the other. Take two orders a cause, the pair of scripts whose order decides the outcome with the same signature and bring the first toward the second and the observable they fight over. The two together turn a by selection: at each position, move the sprite that the second factorial search into a small, complete exploration that ends in order places there leftward by adjacent swaps. A swap that the sort needs exchanges two sprites that the second order has not a diagnosis. yet fixed, and if those two were dependent their conflict edge A. Footprints and dependence would force the same orientation in both orders, which the sort Each sprite has a footprint, a typed record of the resources would already respect, so the swap never crosses a dependent its scripts read, write, create, delete, and consume: variables pair. Every swap is therefore independent, and the two orders and lists, the sprite properties that affect rendering and sensing, are connected by independent swaps. Conversely every acyclic clone families, broadcast channels, and the ordered tokens of orientation is realized by some order: a topological sort of its the random stream and the timer. The typing is what makes directed edges, breaking ties by sprite index, is a permutation the relation precise: a write to one sprite’s position does not whose signature is that orientation. The signature is thus a conflict with a read of another sprite’s score, and the explorer bijection between classes and acyclic orientations, which turns keeps the two sprites apart, while a touch test against a moving the number of classes into a combinatorial quantity, the number sprite reads that sprite’s position and the two stay together. of acyclic orientations of the conflict graph, and tells the A footprint over-approximates by design, in the manner of explorer what to enumerate. a sound abstract interpretation [11]: when a block’s effect Algorithm 1 enumerates one order per class without ever is uncertain, the footprint records the extra accesses, so the materializing Sk . The lemma identifies a class with an acyclic relation errs toward dependence and the reduction stays sound. orientation of the conflict edges, so the explorer walks those In the ball-and-paddle project the paddle’s footprint reads orientations directly. It fixes the conflict edges in an order and the ball’s position and the ball’s footprint writes it, so the two decides them one at a time; at each edge it tries both directions conflict on the ball’s pose and the explorer keeps both orders; and keeps a direction only when the partial orientation a third sprite that only animated a backdrop would conflict so far stays acyclic, which prunes the cyclic combinations that no permutation realizes. When all edges are oriented, with neither and drop out. Two sprites are independent when their footprints do not the canonical linear extension of the resulting partial order, conflict. A conflict is a write against a read or write of the the lexicographically least order consistent with it, is the same resource. Two writes of the same variable through a representative, and the VM runs once on it. Independent pairs commutative operation, such as two scripts that each change a never appear among the edges, so their order is left to the score by one, are exempt from the write-write case, since their canonical extension and never multiplies the work. The cost is what the design is for. The walk visits one leaf order leaves the final value unchanged up to the observation tolerance, which absorbs the low-order differences that floating- per acyclic orientation, and each cyclic prefix is cut the moment point summation introduces. The exemption is local: a script it closes a cycle, so the number of leaves equals the number that both changes and reads the same variable is order-sensitive, of classes and the enumeration is output-sensitive: it runs the because its read observes a different value depending on when VM once per class and not k! times. The acyclicity test and the other write lands, so a read of a commutatively written the canonical extension are a pass over the edges, so the VM resource conflicts. An opcode that the table cannot model runs dominate the cost. A fully dependent set is the worst soundly is given a footprint that conflicts with everything, case, where every order is its own class and the walk reduces nothing; a project whose conflict graph is that dense is capped which keeps the relation an over-approximation. to a sample, the only place the search is not exhaustive. B. The reduced exploration Theorem 2 (Soundness and completeness): Under a footprint Swapping two adjacent independent sprites leaves the that over-approximates the real accesses, with independence observation unchanged, which is the partial-order analog of taken at the grading lens L, every order in a class procommuting two independent events. The equivalence this duces the same observation at L as the class representative, generates on Sk has a clean description: two orders are and the explorer reports an observation for every order in

Algorithm 1 E XPLORE runs the VM once per equivalence Algorithm 2 ATTRIBUTE reduces a difference to its cause by class by walking the acyclic orientations of the conflict graph. subtracting the order sensitivity the paired reference already carries. Require: project P , input ι, seed r, grading lens L Ensure: obs: one witnessing order per distinct outcome 1: g1 , . . . , gk ← contributing sprite targets, stage fixed 2: E ← { (i, j) : i < j, C ONFLICTL (fp(gi ), fp(gj )) } 3: obs ← empty map 4: WALK(1, ∅) 5: return obs 6: procedure WALK(t, ω) 7: if t > |E| then 8: π ← L EX M IN E XTENSION(ω) 9: o ← observe exec(P, ι, r, T0 (π)) at lens L 10: if o ∈ / obs then 11: obs[o] ← π 12: end if 13: return 14: end if 15: (i, j) ← E[t] 16: for d ∈ { i → j, j → i } do 17: if ω ∪ {d} is acyclic then 18: WALK(t + 1, ω ∪ {d}) 19: end if 20: end for 21: end procedure

Sched (P, ι, r, H). No realizable outcome is missed, and no reported outcome is spurious. Soundness comes from the commutation of independent work, with independence the lens-indexed relation C ONFLICTL the explorer computes. Two adjacent sprites it calls independent commute for one of two reasons: their transactions touch disjoint resources, the Bernstein condition [9] under which neither reads what the other writes, or they share only commutatively updated resources whose combined value is order-independent. The second case is value commutativity, not Bernstein independence, so C ONFLICTL admits it only up to the monitor lens, which reads values not operation order, and withholds it at the full-trace lens. Either way the swap preserves the observation at L, and a block move decomposes into such swaps, so the whole reordering preserves it, by induction over the ticks. Completeness comes from Lemma 2. The walk emits one representative per acyclic orientation, every order shares its signature with exactly one orientation the walk emits, and the dynamic creation of clones and receivers adds no ordering freedom because their positions follow from the initial order. The finite ordering choice replaces the unbounded interleaving tree that a general concurrency tester reasons about, which is what lets a single representative settle an entire class. The oracle confirms the lens-bounded exemption loses nothing: the reduced and exhaustive observation sets agree at every lens, including the full-trace lens where the exemption is withheld. The footprint conditions the theorem assumes, over dynamic fan-out, the random and timer streams, unmodeled opcodes, and value-commutative writes, are the soundness contract of Section VI.

Require: control C, suspect M , contended-site descriptor s, lens L Ensure: the observable keys the fault makes order-sensitive, scoped to s 1: Σ ← { identity, reverse, shuffle1 , . . . } 2: for X ∈ {C, M } do 3: b ← keyed observation of exec(X, identity) at lens L 4: DX ← ∅ 5: for σ ∈ Σ \ {identity} do 6: o ← keyed observation of exec(X, σ) at lens L 7: DX ← DX ∪ { κ : o[κ] ̸= b[κ] } 8: end for 9: end for 10: A ← DM \ DC 11: As ← { κ ∈ A : D OWNSTREAM(κ, s) } 12: return As if As ̸= ∅, else A

C. Attributing a difference to its cause A bare difference names two outcomes without explaining them. Algorithm 2 turns the difference into an attribution, a set of observable keys that the order makes the program disagree on, scoped to the pair of scripts responsible. The explorer already records, for each project, which observable keys move under a family of realizable orders. A key names what changed and where: a variable by scope and name, a sprite pose by field, a monitor by identity, a clone by its step in the population trace. The algorithm computes this diverging-key set for the suspect program and for a paired reference, then subtracts. The subtraction is the point. The reference can carry its own order sensitivity, a cosmetic pose that settles differently yet reaches the same result, and subtracting the reference’s diverging keys removes that noise and leaves the keys the fault introduces. A boolean check that only asked whether both programs diverge would do worse: it would miss a fault that moves a different observable than the control, or that enlarges the diverging set, since both programs read as diverging and the boolean attributes nothing. The set difference keeps exactly the observables the fault makes order-sensitive. A non-empty A is the detection, and the run that produced a divergent key is the witness. The scope turns a detection into a localization. The contended-site descriptor names the resource the conflict is about, a variable on a sprite, a pose, or a broadcast and its receivers, and D OWNSTREAM keeps the keys that the descriptor can reach: the exact sprite-and-variable pair, the receiver of a broadcast, the pose of a sprite the conflict actually moves. The discipline is strict, matching the exact pair rather than a shared name, so a same-named variable on an unrelated sprite is not credited. The scoped set As both confirms the fault and points at the two scripts and the resource behind it, which is the information a fix acts on and the localization that Section VII measures. Algorithm 2 needs a paired reference, robust at the grading lens on the benchmark; the set difference still attributes the keys the suspect introduces when the reference carries unrelated order sensitivity. For a corpus project without

a reference, SchedCheck reports the conflicting dependence edge the witness orients, the pair of scripts and the resource the conflict graph already names. D. Keeping the reduction honest Theorem 2 is conditional on the footprint over-approximating reality, and a table that omits an access turns a real dependence into a false independence and a missed outcome. We check the condition with an oracle that does not use footprints at all. For every project with few enough sprites, we run all k! orders, collect the distinct observations, and confirm that the reduced exploration found the same set. A mismatch is a missed outcome and a footprint gap, and the missing outcome is the counterexample that drives the repair, a counterexample-guided refinement of the dependence model [12]. The same oracle validates Algorithm 1 against the brute-force enumeration of Sk : the output-sensitive walk and the k! filter return the same classes on every controlled structure and on a battery of random conflict graphs. The oracle is not a formality. The benchmark passed it, while real projects exposed footprints that under-approximated a real access and so produced false independence. Section VII reports the four corrections they prompted, two from the course corpus, one from the public sample, and one the broadcast and clone reduction surfaced, none of which a constructed benchmark would have surfaced. VI. I MPLEMENTATION SchedCheck runs on the production Scratch virtual machine, scratch-vm 5.0.300 [8], through a headless harness, so a witness it reports is a behavior of the same engine the editor runs. To realize an order it rewrites the project’s layer assignment so the executable targets sweep in that order, then runs the unmodified VM. The same sweep governs the green-flag, broadcast, key, click, and edge fan-out, while clone creation is target-local; that shared layer order is what ties a reported schedule to a remix. No source of the VM is modified; the only addition is the harness that pins nondeterminism and reads the lens projections. The determinism harness installs the pins of Section IV around each run and restores the global state afterward, so runs are independent. The pins are global to the process: the random source, the clock, the identifier counter, and the calendar are shared state of the VM. The exhaustive oracle runs each schedule in its own process, because accumulating runs in one process lets the pins drift, and an early single-process version produced spurious differences that traced to this drift, not to the schedule. The footprint extractor and the conflict predicate implement a typed resource model: a static pass over the block graph maps each opcode to the resource categories it accesses, and two targets are independent when their footprints do not conflict at the lens. A golden test checks the extractor against a reference on a fixture corpus. The lens projections, the explorer, the admissibility gate, and the repair pass build on this core, and the second runtime reuses the explorer and the class enumeration

without change. The observation preserves the identity of each sprite and clone, including the say and think bubbles a sensing fault can make visible. The system is about four thousand lines of JavaScript and Python. The extractor carries a soundness contract. It models variables and lists, the sprite pose and rendering properties, clone families, broadcast channels, and the ordered tokens of the random stream and the timer, and it walks green-flag, broadcast, and clone hats, together with the key and click hats an input timeline triggers. An opcode it does not model is emitted as an external resource that both reads and writes, so an unmodeled construct forces dependence and never a false independence; a target reached only through input or edge hats is treated the same way. The commutative-update exemption applies only to the lenses up to the monitor level, which read values and not the order of operations. VII. E VALUATION We study seven questions. How common is schedulesensitivity in real projects (RQ1)? Is the reduced exploration sound, and how much does it save (RQ2)? Does the tool detect and localize seeded schedule faults (RQ3)? Does schedule perturbation reach faults that input-space testing and static smell checkers leave untouched (RQ4)? Can a detected fault be repaired and re-certified (RQ5)? Is the method parametric in the execution model (RQ6)? Do the schedules the method perturbs occur between real saved copies (RQ7)? A. Setup The corpus is 224 student projects drawn from a Scratch programming course, used as submitted, and we add a uniform random sample of 250 public projects fetched through the Scratch project API as a second, population-level corpus. We run each project under the sound initial-order model to a horizon of thirty ticks, twice on the identity order for the determinism check and then over the realizable orders. For a project with at most five contributing sprites we enumerate all orders; for larger ones we run one representative per dependence class, which the oracle certifies recovers every outcome, so the verdict stays exact where the conflict graph is sparse and samples only the densely coupled remainder. The benchmark holds matched control and mutant pairs for three of the four fault classes: a missing broadcast-and-wait, a read before initialization, and a sensing race on a sprite’s pose, each constructed to pass the admissibility gate of Section IV. A clone-initialization fault is harder to seed as an admissible pair, since the natural mutation changes behavior under every order, so we leave that class to the corpus. The input-gated race of RQ4 is a separate construction. Every measurement runs each schedule in its own process and records the four lens projections. A project enters the prevalence count only when its two identity runs agree exactly, which all 224 satisfy, so a reported difference is a scheduling effect and not residual nondeterminism. We set the horizon at thirty ticks, enough for the green-flag fan-out and the seeded faults to act, and treat the prevalence as a lower bound, since a

difference that appears only past the horizon is undercounted. The soundness check reruns every order where the sprite count is small enough to enumerate and compares the distinct outcomes against the reduced run. B. RQ1: Prevalence

TABLE I S CHEDULE - SENSITIVITY AND THE REDUCTION ACROSS THE TWO CORPORA .

Projects Concurrent Sensitive, final-state lens Reduced = exhaustive (enumerable) Robust projects reduced Footprint gaps the oracle caught

Course

Public

224 162 34 (21%) 142/142 26/127 2

250 108 19 (17.6%) 77/77 40/67 2

Of the 224 projects, 162 have more than one contributing sprite and so admit a scheduling choice; the rest are singlethreaded and robust by construction. At the horizon, 34 of the 162 concurrent projects, 21%, change their finalstate observable under some realizable order, and 40, 25%, deletion before it reached the global random-number stream change a finer observable. The harness reports no project that two sprites both drew from, and a glide-to-sprite step as nondeterministic and no execution error, so these counts whose destination reads a moving sprite’s position, the last attribute the differences to scheduling. Six are sensitive only surfaced only when the reduction reached the broadcast and in their per-tick trace, where a finer rubric than the final state clone fan-out. After the repairs the reduced set of distinct catches what a grader watching the end does not. observations equals the exhaustive set on all 142 course and 77 The figure is exact for the projects we enumerate and a lower public enumerable projects, and where the oracle ever finds a bound for the rest: most concurrent projects have at most five gap it has not yet localized, the tool falls back to the exhaustive contributing sprites and run exhaustively, while a handful are verdict it computes for the check, so the verdict stays sound. larger, one above two hundred sprites, and there we sample Reduction depends on how independent the contributing orders, which can miss a difference but never invent one. The sprites are. The course’s game projects share a small set of sensitive projects span the recurring shapes of Section IV: global variables, a score most often, that many green-flag sprites that read a shared score they also write, senders that scripts update and read, so those pairs stay dependent; the move on before a receiver resets, and sprites that sense a mover broadcast and clone fan-out adds receiver and clone sprites mid-glide. that often act independently, and the reduction prunes their The course is one population, and its rate could reflect one order. Among the robust enumerable projects, 26 of 127 in the cohort. We draw a uniform random sample of 250 public course and 40 of 67 in the public sample reduce below the projects from the Scratch repository and run the same analysis. factorial. Where the graph is sparse the representatives stand Of the 227 that load and run deterministically under the in for the factorial, and a public project whose forty sprites fixed input, 108 have more than one contributing sprite once the model finds independent reduces to a single representative, broadcast and clone fan-out is counted, and nineteen of those, a verdict its 40! orders put out of exhaustive reach. The oracle 17.6%, change a behavioral observable under some realizable cannot enumerate at that size, so the verdict there rests on the order, a variable or a sprite pose differing past a relative dependence model, which we stress with 128 random orders tolerance of 10−6 , three of them races in broadcast fan- on each of the 27 largest projects: the robust verdicts hold and out a green-flag start order alone would miss. Two further every sensitive one surfaces, so the at-scale verdict is sampled projects move only the trailing digits of an accumulating timer, and not merely asserted. floating-point noise from summation order that we do not count; the course corpus has none, its thirty-four sensitive D. RQ3: Detection and localization On the three admissible fault pairs of the labeled benchmark projects all changing a behavioral observable. The matching rate makes schedule-sensitivity a property of how children build the tool detects every fault: a mutant diverges across the initial Scratch programs and not of one classroom. The 23 projects orders at the grading lens while its robust control does not, and our headless runtime cannot load, most carrying custom web admissibility makes that divergence the fault. It also names extensions, stay out of the count; they carry more sprites than the conflicting pair behind each, the broadcast and its receiver, the projects that load, a median of five against two, so the the initializer and the reader, and the mover and the sensor, figure is a lower bound that misses the harder tail. Table I matching the seeded site in all three. Admissibility is itself collects these counts with the soundness and reduction figures divergence under reordering, so detection on these pairs is a lower bar than detection in the wild, which the generated the rest of this section reports. benchmark below corrects. A live logic fault that changes the C. RQ2: Soundness and reduction terminal state under every order perturbs no schedule, so the Soundness is the property a reduced exploration must keep, detector stays silent, separating schedule faults from ordinary and we check it against the independent oracle. Reaching logic faults. The contended pair the tool names is the place a agreement on every enumerable project took four repairs the repair acts on. oracle localized, each a footprint that under-approximated a Enlarging this set from real substrates proves hard: mutating real access: a commutative-update exemption that wrongly every robust concurrent project at every schedule-mutator site, reached a read of the shared score, a touch test that missed the gate admits none of the 265 candidates, an admissible the sensed sprite’s position, a conflict test that settled a clone fault occupying a band a syntactic mutation rarely hits. So we

generate it, 32 programs across the four fault classes, each G. RQ6: Parametricity in the execution model with a designated variable that should reach an intended value, The method depends on the execution model, cooperative a spec fixed by intended behavior and not by divergence under threads over shared state with a single initial-order choice, not reordering. An oracle runs every realizable layer order and on Scratch. We expose this with a second cooperative runtime reads the spec, sorting each program into a schedule fault, whose programs are tasks of read, write, and yield steps started a logic fault that fails under every order, a robust program, in a chosen order. The model-level parts of SchedCheck run or a benign divergence where the order moves a cosmetic on it unchanged, only the footprint extractor and runner being observable while the spec holds; all 32 sort as built. The tool, runtime-specific, and the explorer recovers the same behavior, enumerating the contributing sprites’ layer orders, matches the races, and reduction, matching the oracle. This controlled spec on all 32: it flags every order-dependent program, the eight construction leaves transfer to a production runtime for that schedule faults and the eight benign divergences, and clears runtime to establish. every robust one, detecting every schedule fault across the four classes, including the broadcast fan-out a green-flag start H. RQ7: In-the-wild remixes order alone would miss. The eight benign divergences carry A schedule choice is a hazard only when real saved copies the signal the admissible pairs cannot, an order-dependence realize more than one. Theorem 1 ties every order the explorer that violates no spec, so a sensitivity verdict is necessary and reports to a layer ordering, so the orders that separate a sensitive not sufficient for a fault. project’s outcomes are each a copy a child makes by opening The set-valued attribution is stronger than the boolean check the project and saving it. We find this in the wild: a deployed it replaces: on a pair whose control is itself order-sensitive animation spelling a six-letter logo is schedule-sensitive, its the boolean attributes nothing, the control already diverging six letter-sprites contending for the positions they slide to, so at the grading lens, while the set difference recovers the their start order decides where each lands. The project’s public variable the mutation makes race. On the generated benchmark remix family of over four hundred copies realizes three distinct the attribution names the seeded pair and observable exactly, layer orders of the six sprites, two of which send the letters to precision and recall of eight in eight across the four classes. swapped positions up to four hundred pixels apart, so the logo The localization scales to the corpus without a control: on assembles in one saved copy and scrambles in another. all 34 final-state-sensitive projects the conflict graph names Manifestation is real but uncommon: only the projects with the contended sprite pairs, and the diverging-key set names hundreds of remixes realize a second order, while the long a median of eleven observables per project where a boolean tail with a handful never reorders the contending sprites, since verdict reports one bit. remixing usually adds content, not a layer drag. The fragility is latent, realizable yet rarely hit, which is why a verdict needs E. RQ4: Orthogonality to input and static analysis the complete exploration the oracle backs, not a reliance on Schedule perturbation and input generation address different stumbling into the bad order. axes, and a fault can live in their product: two key-guarded VIII. T HREATS TO VALIDITY scripts are robust with no input, while holding the key opens Construct validity concerns whether a reported witness runs both guards and races the read against the write, which a oneschedule-per-input tool misses and our engine, varying both, on the real VM. Theorem 1 ties every explored schedule to a layer ordering, and the explorer holds the stage as a fixed catches. Static smell checkers miss the same faults from the other suffix, so it never describes a run the VM cannot produce. side. We reimplement three of the bug patterns LitterBox The reduction depends on the footprint over-approximating catalogs that bear on the schedule classes, a variable used the real accesses. We bound this with the independent oracle, before initialization, a global written and read across sprites, which enumerates all orders on small projects and found four and a non-blocking broadcast whose receiver writes shared gaps we repaired, the last surfaced by the broadcast and clone state. Scored against the dynamic verdict they miss five of the reduction; we do not prove it in general. An opcode the table 34 sensitive projects, each a positional or sensing race with no cannot model is given a conflict-with-everything footprint, so smell to name, and flag nineteen robust projects they cannot an unmodeled construct disables reduction and never unsoundly prove safe. Neither view contains the other: a static pattern enables it. Internal validity turns on the constructed benchmark, used raises a suspect, the schedule exploration decides it. only where ground truth is required; prevalence and the F. RQ5: Repair soundness check come from real projects. The admissibility Each repair is a template inverting the fault, a restored gate rules out a logic change masquerading as a schedule fault, broadcast-and-wait or a one-tick wait ahead of the racing read but it aligns with the detector by construction: an admissible so the writer or mover acts first under every order. It adds fault must diverge under some realizable order, what the tool ordering and changes no computed value, so applied to the perturbs, so detection on admissible faults is a lower bar than three benchmark mutants, each becomes schedule-robust at the on faults in the wild. grading lens while still reproducing the control, and the tool The course corpus is the submissions of one course, not a that found the fault certifies its fix. uniform sample of the Scratch population. The random public

sample addresses this and replicates the rate, at the cost of two Schedule-sensitivity also relates to flaky and order-dependent approximations: we stub the project assets, which preserves the tests. A test is flaky when its outcome depends on something the variable, pose, and broadcast logic schedule-sensitivity turns harness leaves unspecified, and test-order dependence and unon but can undercount a race only a costume’s exact shape constrained iteration are recurring causes [16] that dependencyresolves, and we drop the projects whose custom extensions aware test infrastructure tracks [17]. Frameworks detect and our headless runtime cannot load, so the public figure is itself a classify such tests by replaying them under controlled orlower bound. The results hold for one version of the production ders [18]. Schedule-sensitivity is the same phenomenon inside VM; a VM that changed the fan-out or append order would an event-loop block runtime, where the unspecified element is need the realizability argument rechecked, and the determinism the start order of concurrent scripts, and the realizability result check fails safe under such a change. Sensitivity that appears connects the perturbation to a concrete user action, the remix. only past the fixed thirty-tick horizon is undercounted; the Mutation analysis seeds faults to measure a test suite [19], horizon covers the benchmark faults and the early green-flag [20]. We seed similarly for ground truth, with an admissibility behavior, so the prevalence is a lower bound. gate that keeps a seeded fault a schedule fault and discards Two scope choices bound the claims. The realizable space mutants that merely change behavior, in the spirit of filtering is the initial executable-target order, and a schedule that only equivalent mutants [21]. Systematic testing of asynchronous a sub-tick interleaving could produce lies outside it; such an reactive systems explores message and callback orders [22]; interleaving is not reachable by a remix on the production we fix the messages and vary the handler start order, and the VM, so excluding it keeps every reported difference one a finite space lets the exploration be complete. A body of work analyzes block-based programs directly, on real user can hit. The exploration permutes the contributing executable sprite targets under the fixed input timeline; a target a corpus the Scratch repository makes large enough to study first reached through a later broadcast, key, click, edge, or at scale [23]. Test generators drive a project with synthesized clone event inherits the same layer order and introduces no input sequences and check acceptance properties under one second ordering choice. The extractor treats such a target as execution per input [1], [24], [25]; static checkers flag bug conflicting with everything when it cannot model its script, patterns and code smells in the block graph [2], [26], [27]; and and the micro-suite confirms the layer-order model recovers further tools catalog common bugs, verify learner programs, generate hints, debug, and grade homework [28]–[32]. These the freedom these targets carry. The corpus study carries a data-use obligation. The projects target correctness in inputs or code structure, and a single are student work, used under the course’s terms and de- execution per input cannot observe a schedule effect; our work identified: each is keyed by an opaque identifier with author is orthogonal, fixing inputs and perturbing the schedule. Some metadata discarded, and the study records only per-project smell checkers flag the same shapes, a missing wait or an verdicts and never includes a student’s project or name. The uninitialized read, as code patterns the run never confirms, and study observes program behavior, not students, and as an the head-to-head of RQ4 finds neither view contains the other. A recent Scratch-centered line is especially close in domain analysis of programs it falls outside human-subjects review but different in the perturbation it studies. ViScratch uses under our institution’s policy. block code together with gameplay video for automated IX. R ELATED W ORK feedback [33]; Stitch turns feedback into stepwise tutoring [34]; The closest technical lineage is concurrency testing and ScratchEval builds executable tasks and metrics for LLMpartial-order reduction [13]. Stateless model checking explores based block-program repair [35]; EcoScratch studies cost-aware the interleavings of a concurrent program, and dynamic partial- multimodal repair with execution feedback [36]; Raven reorder reduction prunes interleavings that commute [3]. Source thinks Scratch assessment with video-grounded evaluation [37]; sets and optimal reduction tighten the pruning and extend ScratchWorld evaluates executable consequences in Scratch it to dynamically spawned threads [4], against the state worlds [38]; and ScratchLens checks lens-parametric behavioral explosion of interleaved execution [14], on the commutation equivalence between two Scratch programs [5]. Earlier and of Mazurkiewicz trace equivalence [10] and a notion of when parallel work by Zhang and collaborators targets competitiontwo runs count as the same [15]. Our setting is narrower and level feedback, LLM-based Python repair, time-limit-exceeded the narrowing is the point. A Scratch VM is deterministic once errors, merge-conflict resolution, CI-configuration correctness, the initial sprite order is set, so the realizable space is a finite and silent configuration errors [39]–[44]. These works improve symmetric group, and the unbounded interleaving tree of state- feedback, repair, assessment, and analysis over a given program less model checking does not arise. Completeness becomes a or program pair; our contribution isolates a one-program representative cover of that group, with the equivalence classes schedule dimension and gives a complete representative cover characterized by the orientation of conflict edges. The reduction for remix-induced start-order perturbations. is modest in its own right: with independence static and the Our footprint model shares its typed resource accounting with schedule tree of depth one, an optimal dynamic reduction program equivalence. Existing work gives a typed resource would degenerate to enumerating the acyclic orientations, so model and a lens hierarchy for two Scratch programs [5], the contribution is the realizability theorem, the lens lattice, and translation validation [45], regression verification [46], and the lens-bounded commutativity, not a new pruning rule. differential symbolic execution [47], and semantic diffing [48]–

[50], over a syntactic alignment of code [51]–[53], decide whether two programs agree. We reuse that lens hierarchy and resource model to ask whether one program agrees with itself across its schedules. X. C ONCLUSION SchedCheck explores the realizable orders once per dependence-equivalence class and checks the reduction against an exhaustive oracle wherever a project is small enough to enumerate. It finds 21% of concurrent projects schedulesensitive at the grading lens in a course corpus and 17.6% in a random public sample, detects and localizes all three seeded benchmark faults, and instantiates unchanged on a second cooperative event-loop model. The order that flips a result is one a remix can save, so the verdict belongs in the editors and graders millions of learners use.

R EFERENCES [1] A. Stahlbauer, M. Kreis, and G. Fraser, “Testing scratch programs automatically,” in ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE). ACM, 2019, pp. 165–175. [2] G. Fraser, U. Heuer, N. Körber, F. Obermüller, and E. Wasmeier, “LitterBox: A linter for scratch programs,” in IEEE/ACM International Conference on Software Engineering: Software Engineering Education and Training (ICSE-SEET). IEEE, 2021, pp. 183–188. [3] C. Flanagan and P. Godefroid, “Dynamic partial-order reduction for model checking software,” in ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL). ACM, 2005, pp. 110– 121. [4] P. Abdulla, S. Aronis, B. Jonsson, and K. Sagonas, “Optimal dynamic partial order reduction,” in ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL). ACM, 2014, pp. 373– 384. [5] Y. Si and J. Zhang, “ScratchLens: Lens-parametric behavioral equivalence for Scratch programs,” arXiv:2606.15817 [cs.PL], 2026. [6] 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. [7] 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. [8] Scratch Foundation, “Scratch virtual machine (scratch-vm),” https: //github.com/scratchfoundation/scratch-vm, 2024, npm package scratchvm, version 5.0.300, pinned for the experiments. [9] A. J. Bernstein, “Analysis of programs for parallel processing,” IEEE Transactions on Electronic Computers, vol. EC-15, no. 5, pp. 757–763, 1966. [10] A. Mazurkiewicz, “Trace theory,” in Petri Nets: Applications and Relationships to Other Models of Concurrency. Springer, 1987, pp. 278–324. [11] P. Cousot and R. Cousot, “Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints,” in ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL). ACM, 1977, pp. 238–252. [12] 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. [13] P. Godefroid, Partial-Order Methods for the Verification of Concurrent Systems, ser. Lecture Notes in Computer Science. Springer, 1996, vol. 1032. [14] A. Valmari, “The state explosion problem,” in Lectures on Petri Nets I: Basic Models. Springer, 1998, pp. 429–528. [15] R. Milner, Communication and Concurrency. Prentice Hall, 1989. [16] Q. Luo, F. Hariri, L. Eloussi, and D. Marinov, “An empirical analysis of flaky tests,” in ACM SIGSOFT International Symposium on Foundations of Software Engineering (FSE). ACM, 2014, pp. 643–653. [17] M. Gligoric, L. Eloussi, and D. Marinov, “Practical regression test selection with dynamic file dependencies,” in ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA). ACM, 2015, pp. 211–222. [18] W. Lam, R. Oei, A. Shi, D. Marinov, and T. Xie, “iDFlakies: A framework for detecting and partially classifying flaky tests,” in IEEE Conference on Software Testing, Validation and Verification (ICST). IEEE, 2019, pp. 312–322. [19] 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. [20] 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. [21] D. Schuler and A. Zeller, “Covering and uncovering equivalent mutants,” Software Testing, Verification and Reliability, vol. 23, no. 5, pp. 353–374, 2013. [22] A. Desai, S. Qadeer, and S. A. Seshia, “Systematic testing of asynchronous reactive systems,” in ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE). ACM, 2015, pp. 73–83.

[23] E. Aivaloglou and F. Hermans, “How kids code and how we know: An exploratory study on the scratch repository,” in ACM Conference on International Computing Education Research (ICER). ACM, 2016, pp. 53–61. [24] A. Deiner, P. Feldmeier, G. Fraser, S. Schweikl, and W. Wang, “Automated test generation for scratch programs,” Empirical Software Engineering, vol. 28, no. 3, p. 79, 2023. [25] K. Götz, P. Feldmeier, and G. Fraser, “Model-based testing of scratch programs,” in IEEE Conference on Software Testing, Verification and Validation (ICST). IEEE, 2022, pp. 411–421. [26] B. Boe, C. Hill, M. Len, G. Dreschler, P. Conrad, and D. Franklin, “Hairball: Lint-inspired static analysis of scratch projects,” in ACM Technical Symposium on Computer Science Education (SIGCSE). ACM, 2013, pp. 215–220. [27] 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,” Revista de Educación a Distancia, no. 46, 2015. [28] C. Frädrich, F. Obermüller, N. Körber, U. Heuer, and G. Fraser, “Common bugs in scratch programs,” in Innovation and Technology in Computer Science Education (ITiCSE). ACM, 2020, pp. 89–95. [29] A. Stahlbauer, C. Frädrich, and G. Fraser, “Verified from scratch: Program analysis for learners’ programs,” in IEEE/ACM International Conference on Automated Software Engineering (ASE). ACM, 2020, pp. 150–162. [30] F. Obermüller, U. Heuer, and G. Fraser, “Guiding next-step hint generation using automated tests,” in Innovation and Technology in Computer Science Education (ITiCSE). ACM, 2021, pp. 220–226. [31] A. Deiner and G. Fraser, “NuzzleBug: Debugging block-based programs in scratch,” in IEEE/ACM International Conference on Software Engineering (ICSE). ACM, 2024, pp. 1–13. [32] D. E. Johnson, “ITCH: Individual testing of computer homework for scratch assignments,” in ACM Technical Symposium on Computing Science Education (SIGCSE). ACM, 2016, pp. 223–227. [33] 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. [34] 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. [35] Y. Si, S. Han, D. Li, H. Shi, and J. Zhang, “ScratchEval: A multimodal evaluation framework for LLMs in block-based programming,” arXiv:2602.00757 [cs.SE], 2026. [36] Y. Si, M. Wang, D. Li, H. Shi, and J. Zhang, “EcoScratch: Costeffective multimodal repair for Scratch using execution feedback,” arXiv:2603.29624 [cs.SE], 2026. [37] D. Li, D. Li, H. Shi, and J. Zhang, “Raven: Rethinking automated assessment for Scratch programs via video-grounded evaluation,” arXiv:2604.17820 [cs.SE], 2026. [38] Y. Lin and J. Zhang, “ScratchWorld: Evaluating if world models compute executable consequences,” arXiv:2606.31689 [cs.SE], 2026. [39] 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 2022. ACM, 2022, pp. 13:1–13:13. [40] 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. [41] 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. [42] J. Zhang, T. Mytkowicz, M. Kaufman, R. Piskac, and S. K. Lahiri, “Using pre-trained language models to resolve textual and semantic merge conflicts,” in Proceedings of the 31st ACM SIGSOFT International Symposium on Software Testing and Analysis, ser. ISSTA 2022. ACM, 2022, pp. 77–88. [43] M. Santolucito, J. Zhang, E. Zhai, J. Cito, and R. Piskac, “Learning CI configuration correctness for early build feedback,” in Proceedings of the 2022 IEEE International Conference on Software Analysis, Evolution and Reengineering, ser. SANER 2022. IEEE, 2022, pp. 1006–1017. [44] 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. [45] A. Pnueli, M. Siegel, and E. Singerman, “Translation validation,” in Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Springer, 1998, pp. 151–166.

[46] 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. [47] S. Person, M. B. Dwyer, S. Elbaum, and C. S. Păsăreanu, “Differential symbolic execution,” in ACM SIGSOFT International Symposium on Foundations of Software Engineering (FSE). ACM, 2008, pp. 226–237. [48] D. Jackson and D. A. Ladd, “Semantic diff: A tool for summarizing the effects of modifications,” in International Conference on Software Maintenance (ICSM). IEEE, 1994, pp. 243–252. [49] 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 (CAV). Springer, 2012, pp. 712–717. [50] D. A. Ramos and D. R. Engler, “Practical, low-effort equivalence verification of real code,” in Computer Aided Verification (CAV). Springer, 2011, pp. 669–685. [51] J.-R. Falleri, F. Morandat, X. Blanc, M. Martinez, and M. Monperrus, “Fine-grained and accurate source code differencing,” in ACM/IEEE International Conference on Automated Software Engineering (ASE). ACM, 2014, pp. 313–324. [52] 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. [53] 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.