|title:||Design of a verification tool for general public demos|
In our group, we develop program verification tools. These tools take annotated programs as input, and then try to verify whether the program respects the annotations. Unfortunately, it is complicated to demo the ideas behind program verification to people that do not have any programming knowledge.
Nowadays, there is a wide variety of visual programming languages (e.g. Scratch, Processing), which make programming intuitive.
What we would like to investigate in this project is if we could add some form of verification support to such a visual programming language, 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.
In this project, we would like you to investigate the different possibilities that exist to create such a demo-able visual verification environment. It is not necessary that at the end of the project, we have a fully implemented system, but we would like to have a system design.