SMT - Bit Vectors

2020 - Technische Universität München - Master Seminar Thesis


Due to how real computers are designed, SMT formulas built on unbounded integers aregenerally unsuited for deciding properties on program code and instead, sequences of bits,calledbit vectors, are used to represent machine integers. After establishing a calculus forSMT formulas on such data, this document elaborates on how these can be automaticallydecided by using theflatteningapproach to translate them into propositional logic, which canbe solved by any SAT solver. This approach is extended toincremental flattening, which isable to decide certain types of formulas significantly faster. For these processes, an exemplarilyimplementation in Haskell is developed, which is finally being used to solve a small CrackMe-challenge as an example application.

Additional Resources:

Volume Rendering of Meteorological Simulation Data

2018 - Technische Universität München - Bachelor’s Thesis in Informatics: Games Engineering


This thesis presents the integration of two different volume lighting methods to be used for visualization of meteorological simulation data, in particular cloud data, in Met.3D, an open-source visualization application for meteorological uses. The first method is primarily a visuals-based approach, which simulates single scattering and imitates certain visual phenomena appearing in real-world clouds. The second, while generally requiring more computational effort, is a specific implementation of the photon mapping algorithm and directly simulates multiple scattering by tracing photons through the volume. It takes advantage of the Henyey-Greenstein function in order to be able to only use 3D textures as the data structure of the photon map. We use our implementations of these methods to produce a number of images and analyze them with respect to visual outcome, physical accuracy and performance. In addition, we compare images created with the photon mapping method to results that were generated using MFASIS, a method to simulate radiative transfer of clouds.

Additional Resources:

Case Study on LLVM as suitable intermediate language for binary analysis

2017 - Technische Universität München - Bachelor Seminar Thesis


Many binary analysis tools and compilers, instead of directly working on code, use an intermediate representation of it. The idea of this thesis is to use the well-tested intermediate representation from LLVM for binary analysis tasks. We take a look at McSema, a tool to translate x86 and x86_64 binaries to LLVM, describe its translation process in detail and additionally implement Python bindings for it. To practically test McSema, we present five examples of code we translate to LLVM and then recompile again. The last of these demos is an example on using KLEE, a symbolic execution engine for LLVM, on the code produced by McSema in order to successfully solve a CrackMe. We conclude that McSema's translation approach provides a suitable way to extract functions from binaries to integrate them in other code or to analyse them using symbolic execution, as well as serving as a potential basis to implement an LLVM-based decompiler. We also compare it to Remill, another tool similar to McSema, which generates code that represents the assembly code more explicitly and VEX, the intermediate representation used in Valgind and Angr, which is also more close to the machine code.

Additional Resources:

Umwandlung von Bildern in Audio-Signale

2013 - Gymnasium Penzberg - German only

Die Arbeit steht unter einer Creative Commons Namensnennung - Nicht-kommerziell - Weitergabe unter gleichen Bedingungen 3.0 Unported Lizenz, das zugehörige Programm unter der GPLv3.

Arbeit als PDF

Programm "audiocrypt":

Es werden folgende Libraries benötigt: FreeImage, FreeImagePlus (i.d.R. in FreeImage enthalten), libsndfile.
Dem Windows Binary liegen die jeweiligen DLLs bereits bei.