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 Fall 2026.
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
Extracting Block I/O Stream Representations from Filesystems (Roshan Nair)
Applications issue file-level operations, but an SSD observes the block I/O produced after the filesystem has transformed those operations. Journaling, metadata updates, copy-on-write, allocation, and cleaning can introduce new writes, redirect existing ones, and change their spatial and temporal patterns. Consequently, the same application can produce substantially different device-level workloads on ext4, XFS, F2FS, or Btrfs. Detailed block traces expose these differences, but they are difficult to interpret, compare, or reuse. This project investigates whether a filesystem-mediated workload can instead be represented by a minimal set of block I/O streams that preserves the characteristics most relevant to SSD behavior and write amplification.
What you will learn:
- How the Linux storage stack and filesystems shape block I/O.
- How SSD internals interact with I/O patterns and cause write amplification.
- How to benchmark and trace storage systems and identify steady state.
What you will do:
- Characterize the block I/O produced by two filesystems, such as ext4, XFS, F2FS, or Btrfs, under representative applications and benchmarks.
- Determine which filesystem and workload parameters—such as journal mode, mount options, allocation policy, I/O size, and synchronization behavior—meaningfully affect steady-state device-level I/O.
- Derive a minimal set of block I/O streams that captures the steady-state behavior of each filesystem-mediated workload.
References:
- Lee et al., F2FS: A New File System for Flash Storage, FAST 2015.
- Kang et al., The Multi-streamed Solid-State Drive, HotStorage 2014.
- Rho et al., FStream: Managing Flash Streams in the File System, FAST 2018.
SSD-Aware RL for Data Placement in Storage Systems (Roshan Nair)
Reinforcement learning has shown promise for data placement in storage systems (Sibyl, Harmonia, etc.), but existing approaches typically treat SSDs as black boxes and optimize only observed latency. This ignores internal signals such as garbage collection activity, write amplification, utilization, and wear, even though placement decisions directly affect them. This project investigates whether exposing SSD-internal state to the agent and optimizing jointly for performance, write amplification, wear balance, and energy can produce better placement policies for heterogeneous SSD arrays.
What you will learn:
- How SSD internals, including the FTL and garbage collection, shape performance, write amplification, and device wear.
- How to formulate a systems problem as a reinforcement-learning problem by designing meaningful state, action, and reward spaces.
- How to evaluate learned placement policies rigorously against handcrafted baselines across heterogeneous storage configurations.
What you will do:
- Reproduce an RL-based data-placement baseline on heterogeneous SSDs and compare it with simple heuristic policies.
- Extend the agent with SSD-internal signals, such as garbage collection activity, write amplification, utilization, and other device statistics.
- Design and evaluate rewards that balance performance, write amplification, and wear across heterogeneous SSD-backed systems.
References:
- Singh et al., Sibyl: Adaptive and Extensible Data Placement in Hybrid Storage Systems Using Online Reinforcement Learning, ISCA 2022.
- Nadig et al., Harmonia: A Multi-Agent Reinforcement Learning Approach to Data Placement and Migration in Hybrid Storage Systems, 2025.
- Bera et al., Pythia: A Customizable Hardware Prefetching Framework Using Online Reinforcement Learning, MICRO 2021.
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