Write a Blog >>
ASE 2020
Mon 21 - Fri 25 September 2020 Melbourne, Australia
Tue 22 Sep 2020 09:10 - 09:30 at Kangaroo - Formal Methods (2) Chair(s): Eunsuk Kang

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.

Tue 22 Sep
Times are displayed in time zone: (UTC) Coordinated Universal Time

09:10 - 10:10: Formal Methods (2)Research Papers at Kangaroo
Chair(s): Eunsuk KangCarnegie Mellon University, USA
09:10 - 09:30
Talk
Verified from Scratch: Program Analysis for Learners' Programs
Research Papers
Andreas StahlbauerUniversity of Passau, Christoph FrädrichUniversity of Passau, Gordon FraserUniversity of Passau
09:30 - 09:50
Talk
Interval Change-Point Detection for Runtime Probabilistic Model Checking
Research Papers
Xingyu ZhaoHeriot-Watt University, Radu CalinescuUniversity of York, UK, Simos GerasimouUniversity of York, UK, Valentin RobuHeriot-Watt University, David FlynnHeriot-Watt University
Pre-print
09:50 - 10:10
Talk
UnchartIt: An Interactive Framework for Program Recovery from Charts
Research Papers
Daniel RamosINESC-ID/IST, Universidade de Lisboa, Jorge PereiraINESC-ID/IST, Universidade de Lisboa, Ines LynceINESC-ID/IST, Universidade de Lisboa, Vasco ManquinhoINESC-ID/IST, Universidade de Lisboa, Ruben MartinsCarnegie Mellon University