Pierre Donat-Bouillud, Ph.D.

Pierre Donat-Bouillud, Ph.D.

Sebastián Krynski, MSc.

Department of Theoretical Computer Science

Symbolic execution is a technique that enables one to test programs and prove nontrivial properties about a program. Making a new symbolic execution engine is challenging. Instead, a technique is used where an interpreter of the target language is symbolically executed itself, simplifying the symbolic execution of its programs. In this work, I show how to apply this to the R language. The resulting symbolic execution engine can be used to, for example, test library correctness or generate type annotations.

Thesis on DSpace

Pierre Donat-Bouillud, Ph.D.

Ing. Stanislav Kuznetsov, Ph.D.

Department of Software Engineering

Automated grading systems for programming courses face challenges in security and test rigour, particularly for advanced topics like program testing tools. This thesis introduces Fittest, a new automated grading system designed to address these challenges. It employs a secure hybrid architecture, where student code runs on GitLab CI but critical grading logic occurs on a protected backend server. Fittest supports dynamic C program generation for evaluating student-developed code coverage tools and fuzzers, and integrates with university authentication. The result is a secure and pedagogically sound assessment platform for the NI-APT course.

Pierre Donat-Bouillud, Ph.D.

Ing. Petr Máj, Ph.D.

Department of Software Engineering

This thesis addresses the critical challenge of reproducibility in computational research conducted through R notebooks. While R notebooks have revolutionized scientific workflows by integrating code, narrative, and results, their outputs often vary across different execution environments due to dependencies on library versions, operating systems, and time-dependent operations. Traditional comparison tools like GNU Diff fail to capture meaningful differences in dynamic outputs such as plots and statistical tables. This research develops and evaluates a semantic diff tool specifically designed for R notebooks that can detect differences beyond textual comparison. Through comprehensive analysis of the R programming language and notebook ecosystem, a tool was implemented that computes similarity metrics (including DSSIM and relative difference) for outputs suspected to be semantically equivalent. Evaluation across varied computational environments demonstrated the tool's ability to identify meaningful differences that conventional text-based comparison would miss, particularly in complex outputs like data visualizations and statistical tables. Despite its effectiveness, opportunities remain for improving computational efficiency, particularly in output generation speed and optimization of the Top-Down computation phase. This work contributes to reproducibility science by enabling more sophisticated comparison of notebook outputs, advancing transparency and reliability in computational research.

Pierre Donat-Bouillud, Ph.D.

prof. Christoph Kirsch

Department of Theoretical Computer Science

The thesis evaluates techniques for tackling path explosion in symbolic execution. There is a particular focus on the interaction of the techniques with nested loops. Path pruning, path subsumption, state merging, and loop summarization techniques are discussed using examples. Symbolic execution and these techniques are implemented to analyze programs written in an educational language called microc, a language inspired by C. The thesis describes experiments performed to compare the techniques, especially to find out how well the techniques deal with many loops or deep nested loops. A random microc program generator is developed to experiment with the symbolic executor.

Thesis on DSpace

Pierre Donat-Bouillud, Ph.D.

Ing. Josef Gattermayer, Ph.D.

Department of Theoretical Computer Science

Vyper is a programming language for writing smart contracts on EVM-based blockchains. Smart contracts can hold up to billions of dollars; thus, security is the highest priority. Historically, the Vyper compiler contained multiple bugs that affected the production contracts and eventually led to a major hack. This thesis covers the topic of compiler testing with a focus on testing the Vyper compiler. It implements an AST interpreter for Vyper and uses it to differentially fuzz the compiler. The approach is tested with feasibility experiments where two old Vyper bugshigh and medium severityare ported to the current version, and the fuzzer is targeted to find them. The experiments showed that the fuzzer can quickly detect them and thus can be used to improve the correctness of the compiler.

Thesis on DSpace