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
- firstname.lastname@sosy.ifi.lmu.de
- ORCID
-
0009-0008-7961-190X
Thesis Mentoring
Available topics
Comparing CEGAR with Trace Abstraction and Predicate Abstraction [1, 2, 3]
Trace abstraction and predicate abstraction are two state-of-the-art domains utilized by Counterexample-Guided Abstraction Refinement (CEGAR). One is implemented in CPAchecker and the other one in UAutomizer. The open question is which of the abstraction allows CEGAR to do less refinements when fixing the same external factors. This thesis aims to compare the two CEGAR implementations in CPAchecker and UAutomizer when fixing the same search algorithm and SMT solver.
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.