Semantics, Modelling and Verification

Master thesis
Author: Marvin Fourastié
Language: English
Document available here

Abstract

The teaching of computer science has become essential in the majority of educational programs. Therefore, many programming languages were born with the will to propose a first programming experience to beginners, usually through sequences of instructions to execute. However, the programming language FunBlocks explores another approach focusing on state transformations based on term rewriting systems. Additionally, it is an educative programming language providing a visual interface inspired by block programming. The rewriting theory allows the user to create rules consisting in transform string of symbols (called terms) into other ones. Term rewriting has its own theory and contains some properties that are interesting for the learning of computer science. As the majority of these properties are undecidable in general, many verification tools exists, but there are not well suited for an educative purpose.

In an effort to provide an adapted response, we propose the FunBlocks checker that is a verification tool working on FunBlocks. Our tool aims to give the user the possibility to check two important properties, namely termination and confluence, using a simple command line interface. To do this, we use Maude, a language following the rewriting theory and containing a formal environment which can check if no infinite derivation exist (termination) or if each term has at most one normal form (confluence). The goal is to offer an extra educational value to FunBlocks by providing intuitive feedback emphasising on important properties in computer science, though the use of rewrite rules.

Master thesis
Author: Patrick Sardinha
Language: French
Document available here

Abstract

La programmation graphique permet de créer des applications 3D et est notamment utilisée pour la conception de jeux vidéo ainsi que pour la modélisation. A l’heure actuelle, la spécification OpenGL est l’une des plus utilisées pour la création d’applications graphiques et offre un ensemble de fonctions donnant la possibilité aux programmeurs de déclarer et de manipuler des objets 3D ainsi que des images. Cependant, l’utilisation d’une telle spécification demande de coder à relativement bas niveau et de bonnes connaissances dans la programmation graphique. Il est de ce fait assez compliqué de concevoir ce type d’applications. L’utilisation d’un langage de programmation haut niveau incluant des abstractions sur les types est un moyen de faciliter la conception de ces dernières. Le but de ce travail est de créer un nouveau langage nommé PATL, ayant pour but d’être complètement déclaratif, de proposer une implémentation par blocs et de permettre l’utilisation d’abstractions pour la création des applications et la représentation des objets 3D. Il s’agit d’un \textit{Domain-Specific Language} (DSL) orienté Swift inspiré d’un langage déclaratif: React. Ce nouveau langage de programmation a pour but de permettre la création et l’utilisation de types abstraits et d’ajouter une couche déclarative à Rendery, un moteur de rendu 2D/3D moderne qui est écrit en Swift et basé sur OpenGL. L’utilisation de PATL avec Rendery vise à ne pas avoir à manipuler les fonctions OpenGL et ainsi de créer des applications graphiques de manière simplifiée tout en utilisant le langage Swift.

Bachelor thesis Authors: Deniz Sungurtekin and Matthias Tonini Language: French Deniz’s thesis is available here, Matthias’ here.

Abstract

Les drones seront de plus en plus présents dans nos vies. De nos jours, les drones sont déjà utilisés pour de nombreuses activités différentes telles que l’agriculture, la prise de vidéo pour des films/vidéos/documentaires, la recherche de survivants, etc. À l’avenir, les drones prendront encore plus de place dans nos vies. Les entreprises de livraison cherchent à les utiliser afin de pouvoir livrer des colis à moindre coût et plus rapidement, les systèmes de santé se penchent sur leur possible utilisation en tant qu’ambulances. Les domaines dans lesquels les drones peuvent être utiles semblent ainsi infinis.

L’objectif de ce travail est d’apporter une nouvelle utilisation aux drones: les utiliser dans un but éducatif, notamment dans le milieu de la programmation. Ce travail consiste donc principalement au développement d’une application iOS qui permet la programmation en bloc de plans de vol et le test ainsi que la simulation de ces plans de vols avant leur exécution par le drone.