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

Displayed time zone: (UTC) Coordinated Universal Time change

09:10 - 10:10
Formal Methods (2)Research Papers at Kangaroo
Chair(s): Eunsuk Kang Carnegie Mellon University, USA
Verified from Scratch: Program Analysis for Learners' Programs
Research Papers
Andreas Stahlbauer University of Passau, Christoph Frädrich University of Passau, Gordon Fraser University of Passau
Interval Change-Point Detection for Runtime Probabilistic Model Checking
Research Papers
Xingyu Zhao Heriot-Watt University, Radu Calinescu University of York, UK, Simos Gerasimou University of York, UK, Valentin Robu Heriot-Watt University, David Flynn Heriot-Watt University
UnchartIt: An Interactive Framework for Program Recovery from Charts
Research Papers
Daniel Ramos INESC-ID/IST, Universidade de Lisboa, Jorge Pereira INESC-ID/IST, Universidade de Lisboa, Ines Lynce INESC-ID/IST, Universidade de Lisboa, Vasco Manquinho INESC-ID/IST, Universidade de Lisboa, Ruben Martins Carnegie Mellon University