Marek Jankola
Software and Computational Systems Lab
Department of Computer Science
Ludwig-Maximilians-Universität München (LMU Munich)
Oettingenstraße 67
80538
Munich
(Germany)
- Office
- Room F 006, Oettingenstr. 67
- marek.jankola@sosy.ifi.lmu.de
- ORCID
-
0009-0008-7961-190X
Thesis Mentoring
Available topics
Creating Benchmarks for SV-Comp with TransVer [1]
TransVer is a framework for program instrumentation. It can reduce verification of different properties to reachability. Some reachability verifiers do not perform very well on the transformed tasks. One of the ways to motivate reachability analyzers to improve on these tasks is to create benchmarks and add them to SV-Comp.
Reduction of Termination to Reachability for Recurrent Programs in TransVer [1]
TransVer is a framework for program instrumentation. It can reduce verification of different properties to reachability. It can handle termination reduction but it is limited for recurrent programs. Goal of this thesis is to adapt the transformation for the programs with recursion.
Reduction of Termination to Reachability for Programs with Arrays in TransVer [1]
TransVer is a framework for program instrumentation. It can reduce verification of different properties to reachability. It can handle termination reduction but it is limited for programs with arrays. Goal of this thesis is to adapt the transformation for the programs with arrays.
If you're a student interested in writing your thesis at our chair, you should also have a look at our full list of currently available theses.