Below are topics offered by DSLAB for Bachelor and/or Master projects/theses. If you have already been admitted to the doctoral program and are interested in a Ph.D. semester project, please email Prof. Candea directly.
Please read our projects guide to understand how we supervise projects in DSLAB, what we expect from students, the formal requirements, and the grading scheme.
DSLAB works on computer systems, with some formal methods and networks as well. You can therefore think of our projects as extensions of courses like EPFL’s Operating Systems (CS-323), Software Engineering (CS-305), Systems-Oriented Programming (CS-207), and/or Computer Networks (COM-208). To be productive and happy doing our projects, you must be enthusiastic about these subjects and must have done very well in these (or equivalent) courses. Learning on the fly is both encouraged and necessary, but in a semester project there is limited time to learn things you could have learned from courses, hence the need for existing knowledge and skills. For example, you should not find low-level programming like C/Rust and the notions of stack/heap/pointers intimidating.
To do a Master thesis in DSLAB, you must have already taken the Principles of Computer Systems course.
The following list is for Spring 2025.
If interested, e-mail us at projects@dslab.org
- one paragraph of motivation explaining which project(s) interest(s) you and why
- your résumé (curriculum vitae)
- a grades transcript
Profiling Automated Verifiers
Automated and semi-automated tools for formal verification extensively use SMT solvers as a backend for proof automation. While SMT solvers promise to lower the amount of effort and expertise required for verification, in practice their lack of performance predictability and debuggability poses significant usability challenges for users and developers of SMT-based verifiers (e.g., Dafny), as well as negatively impacting the performance of symbolic executors (e.g., KLEE). This project explores how we can help developers pinpoint the root causes of performance issues in automated verifiers using a special-purpose profiler.
In this project, you will:
- Build a profiler that identifies the portion of solving time spent on each task across the verifier stack, which comprises for instance the symbolic executor and the SMT solver.
- Come up with practical ways to distinguish between useful versus useless work done, as well as brute-force search versus precise reasoning.
- Evaluate the usability of your profiler on pinpointing the root cause of real-world verifier performance issues.
You will learn:
- Internals of industrial-grade SMT solvers like Z3 and CVC5, as well as symbolic executors like KLEE.
- Profiling techniques
Your own idea
Do you have a project idea related to DSLAB’s interests, such as dependability or practical formal verification?
Feel free to contact us!
In this project, you will:
- Work on your own idea with our guidance
- Discover something new, small or large
You will learn:
- Something you don’t know already