Bachelor theses
Symbolic execution for R
Author
Petr Šťastný
Year
2024
Type
Bachelor thesis
Supervisor
Pierre Donat-Bouillud, Ph.D.
Reviewers
Sebastián Krynski, MSc.
Department
Summary
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.
Master theses
Nested loops and path explosion in symbolic execution
Author
Vojtěch Rozhoň
Year
2024
Type
Master thesis
Supervisor
Pierre Donat-Bouillud, Ph.D.
Reviewers
prof. Christoph Kirsch
Department
Summary
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.
Interpretation and Differential Fuzzing of the Vyper Language
Author
Miroslav Škrabal
Year
2025
Type
Master thesis
Supervisor
Pierre Donat-Bouillud, Ph.D.
Reviewers
Ing. Josef Gattermayer, Ph.D.
Department
Summary
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.