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.