Rust is a systems programming language that guarantees both performance and Memory Safety through its memory model. With unsafe rust it is possible to opt-out of some security guarantees made by the compiler. However, this comes at the risk of re-introducing memory bugs. While various tools already exist for detecting memory errors in (unsafe) Rust, they are either dynamic or focus on proving the absence of bugs. In this thesis we lay the foundations for a static analysis for Rust that focuses on proving the presence of bugs (Under Approximation) instead of their absence (Over Approximation). We show how we can use a formal framework called incorrectness separation logic (ISL) to show the presence of memory errors in Rust. We add Rust support to Infer, a static analysis tool by Meta that uses ISL to prove the presence of bugs. This is done by translating Rust to a Verification Intermediate Language. Finally, we show that our extension to can be used to detect memory bugs in Rust such as null pointer dereferences, dangling pointer dereferences and use after frees.

Dataset: https://doi.org/10.4121/f0b3b808-51c3-4637-b6ff-3654506da71c

Elderly care residences often have falling incidents, sometimes with dire consequences. This project aims to implement a method for detecting when people fall, an issue that has seen much research and practical implementations already. In contrast to other work, this project aims to create a non-intrusive, non-wearable solution through the use of cameras. It extends an existing patient monitoring system developed by Eya Solutions, a start-up in the medical field. Their system monitors patients and is composed of embedded systems (clients), a back-end with a database, and a web-based dashboard (the front-end) for administrators, caretakers and users. Our client wants to extend their system by introducing: (i) a video processing component which performs face recognition, (ii) functionality for indoor positioning of people, (iii) functionality to automatically determine near-optimal placement of cameras, and (iv) automatic detection of fall incidents. To understand the relevant research, we survey the field investigating five key research topics: (i) object detection, (ii) fall detection, (iii) facial recognition, (iv) floor plan modelling, and (v) camera placement optimisation. The first part of the project is detecting fall incidents in video footage. By means of image processing (in particular, subsequent frame subtraction), our system detects objects in the foreground and tracks these between frames. Based on the properties of such objects, namely size and shape, we detect fall incidents. The second part of the project is the floor plan editor. This editor is integrated into the existing dashboard, where administrators can model the building. Eya Solutions wishes to provide the product to customers as a complete package, including (i) showing where fall incidents have occurred, and (ii) how and where to place cameras. Our system allows administrators to edit the floor while allowing caretakers to see the modelled floor and see where falls are detected. Considering (ii), it is desirable to generate a configuration where the number of cameras is low while the view coverage is high. Our contribution includes a genetic algorithm which can generate automatically a suitable configuration. Alternatively, cameras can be placed manually by the administrator.