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.

Andreas Stahlbauer

University of Passau

Germany

Christoph Frädrich

University of Passau

Gordon Fraser

University of Passau

Germany

Recent probabilistic model checking techniques can verify reliability and performance properties of software systems affected by parametric uncertainty. This involves modelling the system behaviour using \emph{interval Markov chains}, i.e., Markov models with transition probabilities or rates specified as intervals. These intervals can be updated continually using Bayesian estimators with imprecise priors, enabling the verification of the system properties of interest at runtime. However, Bayesian estimators are slow to react to sudden changes in the actual value of the estimated parameters, yielding inaccurate intervals and leading to poor verification results after such changes. To address this limitation, we introduce an efficient interval change-point detection method, and we integrate it with a state-of-the-art Bayesian estimator with imprecise priors. Our experimental results show that the resulting end-to-end Bayesian approach to change-point detection and estimation of interval Markov chain parameters handles effectively a wide range of sudden changes in parameter values, and supports runtime probabilistic model checking under parametric uncertainty.

Xingyu Zhao

Heriot-Watt University

United Kingdom

Radu Calinescu

University of York, UK

United Kingdom

Simos Gerasimou

University of York, UK

United Kingdom

Valentin Robu

Heriot-Watt University

David Flynn

Heriot-Watt University

Charts are commonly used for data visualization. Generating a chart usually involves performing data transformations, including data pre-processing and aggregation. These tasks can be cumbersome and time-consuming, even for experienced data scientists. Reproducing existing charts can also be a challenging task when information about data transformations is no longer available.

In this paper, we tackle the problem of recovering data transformations from existing charts. Given an input table and a chart, our goal is to automatically recover the data transformation program underlying the chart. We divide our approach into four steps: (1) data extraction, (2) candidate generation, (3) candidate ranking, and (4) candidate disambiguation. We implemented our approach in a tool called UnchartIt and evaluated it on a set of $50$ benchmarks from Kaggle. Experimental results show that UnchartIt successfully ranks the correct data transformation program in the top-10 in $92%$ of the instances. To disambiguate those programs, we use our new interactive disambiguation procedure, which successfully returns the correct program on 98% of the ambiguous instances by asking on average fewer than 2 questions to the user.

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

United States