Verified from Scratch: Program Analysis for Learners' Programs
Block-based programming languages like Scratch support learners by providing high-level constructs that hide details and by preventing syntactically incorrect programs. Questions nevertheless frequently arise: Is this program satisfying the given task? Why is my program not working? To support learners and educators, automated program analysis is needed for answering such questions. While adapting existing analyses to process blocks instead of textual statements is straightforward, the domain of programs controlled by block-based languages like Scratch is very different from traditional programs:
In Scratch multiple actors, represented as highly concurrent programs, interact on a graphical stage, controlled by user inputs, and program statements mainly determine visual aspects and movement.
Analyzing such programs is further hampered by the absence of clearly defined semantics, often resulting from ad-hoc decisions made by the implementers of the programming environment.
To enable program analysis, we define the semantics of Scratch using an intermediate language. Based on this intermediate language, we implement the Bastet program analysis framework for Scratch programs, using concepts from abstract interpretation and software model checking.
Like Scratch, Bastet is based on Web technologies, written in TypeScript, and can be executed using NodeJS or even directly in a browser.
Evaluation on 272 programs written by children suggests that Bastet offers a practical solution for analysis of Scratch programs.
Conference DayTue 22 SepDisplayed time zone: (UTC) Coordinated Universal Time change
09:10 - 10:10
|Verified from Scratch: Program Analysis for Learners' Programs|
|Interval Change-Point Detection for Runtime Probabilistic Model Checking|
Xingyu ZhaoHeriot-Watt University, Radu CalinescuUniversity of York, UK, Simos GerasimouUniversity of York, UK, Valentin RobuHeriot-Watt University, David FlynnHeriot-Watt UniversityPre-print
|UnchartIt: An Interactive Framework for Program Recovery from Charts|