Description

Nowadays, there is a wide variety of visual programming languages which makes programming intuitive and easy to get started. In particular, Scratch and Snap! are popular languages to teach programming to children.

We would like to investigate how we can use such programming languages to demo the program verification technology that we are developing within our research group. Concretely, we would like to investigate if we can add some form of verification support to Snap!, in such a way that (1) the program annotations become a part of the programming language, and (2) we have basic support to check whether the program respects the annotations.

We would like you to investigate the different possibilities that exist to create such a demo-able visual verification environment.

Final paper: https://drive.google.com/file/d/1tmyqAjSB_xd82cu1Dj-xDRALHvx3D3L9/view