MSc Defences Fall 2022

Study Programme  

Computer Science

Title  

Analysing the cognitive effectiveness of the DCR graphs visual notation

Abstract  

Business process modelling languages are one of many tools enabling institutions to document, simulate, and optimise processes. DCR especially is a rapidly growing modelling language used by both professionals and novices of varying backgrounds and domain knowledge.
Building on previous research, this exploratory study documents the development of notation updates aiming to improve the notation effectiveness, specifically in context of novice users. The altered notation elements were developed based on the Physics of Notations framework providing guidelines and evaluation metrics. Subsequently, a pilot study with external participants was conducted to evaluate the effects of the updated notation and to gain user insights for further development of the notation changes.

Supervisor(s)  

Hugo Andrés López and Tijs Slaats

External examiner(s)  

Søren Debois

Date and time  

20.09.2022 14:00

Room  

SCI-DIKU-sigurdsgade-2-03

Study Programme  

Computer Science

Title  

Controlling a UR5e robot through a simulated environment using motion imitation of human movement

Abstract  

Simulation of motion data has grown rapidly in recent years. It is not
confined to a single area but can be found in applications from games
to industry. One area is the simulation of data across different bone
structures. However, this distinct problem raises several issues such as
how to relate the reference points on bones and how to avoid creating
unintended collisions.

The goal of this research is to design and implement a solution that can
simulate motion data recorded by an external source and apply it to a
physical entity. For this purpose, a pair of rokoko smart gloves, UR5e
robotic arm, and Tiny Differentiable Simulator is used.

The reader will be presented with a broad overview of the research area
through a literature study, a potential design of a system, together with
an overview of the implementation. Limitations and flaws of the implementation are highlighted and potential areas for future work are identified to the reader.

Keywords: Motion imitation, trajectory optimization, motion retargeting, robotics, simulation, literature review.

Supervisor(s)  

Kenny Erleben

External examiner(s)  

Morten Skov

Date and time  

23.09.2022 14:00

Room  

UP1, room 3.2.07

Study Programme  

Computer Science

Title  

A Simple Verification-condition Generator

Abstract  

Hoare logic is a deductive system consisting of a set of axioms and inference rules from which we can argue about the correctness of programs. In this thesis we present a system for deductive verification
of programs through automated generation of proof obligations based on such logic. In particular, we first extend a basic while-class language to support partial operators such as division and recursive
procedures with parameters and local variables. In order to reason about the partial correctness of programs in our language, we present a Hoare logic which we formally prove sound. Based on this we develop a verification-condition system and also formally prove this sound and complete (with respect to our presented Hoare logic). To accompany our language we implement a parser, interpreter and verification-condition generator (VCG) capable of interfacing to a SMT-LIB solver. Finally, we
test the VCG on both iterative, recursive, valid and invalid (with respect to pre- and post-conditions) annotated programs.

Supervisor(s)  

Andrzej Filinski

External examiner(s)  

Mads Rosendahl

Date and time  

07.10.2022 09:00

Room  

PLTC meeting room