Valentin Aebi

   

Interests Background Projects

Master's student in computer science at EPFL, currently doing research in type systems for my master's thesis


Interests


Background and experience


Projects

  Immediate tracing for Java programs  

Research project, EPFL SYSTEMF laboratory, 2023-2024

Keywords: Java compiler plugin, JVM bytecode, Debuggers, Program tracing

For my master semester projects, I contributed to SYSTEMF's Immediate tracing project, whose goal is to record the evolution of the state of a program and display it as an execution trace. My work was focused on implementing such a tool for Java. The first version was based on bytecode instrumentation (report). The second version consists of a plugin for the Java compiler.


  The Rattlesnake programming language  

Personal project, started in 2022

Keywords: Language design, Compiler, JVM bytecode, Scala

Simple imperative programming language, compiled to JVM bytecode by a compiler written in Scala. It started at the end of my bachelor's as a mean for me to learn more about compilers, and evolved into a platform for small experiments in language design. The language is small, but provides enough features to write meaningful programs of several hundreds of lines of code (see the sudoku solver in this list). Its features include arrays, nominal structures and interfaces, smart casts, and (shallow) mutability control. Its main limitations are the lack of IOs (the only one being prints to the console), the absence of a module system (all functions are top-level), the non-interoperability with other JVM-based languages, and the absence of closures and higher-order functions.


  Symbolic execution engine for Java bytecode  

Personal project, started in 2024

Keywords: Bug detection, Z3 SMT solver, JVM bytecode, Kotlin

A bug detection engine for Java-based languages, written in Kotlin. It uses symbolic execution to compute feasible paths in methods and detect errors like null dereferences, out-of-bound array accesses, and divisions by zero. It is currently an early prototype due to lack of time to work on it. In its current state, the engine is able to perform intra-procedural analysis and to generate methods summaries. The actual usage of method summaries for inter-procedural analysis is however not (yet) implemented.


  Verifying compiler for Rattlesnake  

Course project, Fall semester 2022

Keyword: Program verification, Formal methods, Z3 SMT solver, Scala

As part of EPFL's Formal verification class, we had to complete a project related to formal methods. My teammates and I chose to implement a verifying compiler for a subset of Rattlesnake, a language that I had created as a free-time project. Our verifier is able to check Rattlesnake programs that use integers and booleans. We have been able to prove simple properties like the absence of out-of-bounds errors in array iterations. Due to time constraints, we had to limit ourselves to sound approximations about values loaded from arrays and structures.


  Stoichiometry calculator  

Personal project, 2022

Keywords: Linear algebra, Chemistry, Rust

A calculator to balance chemical equations and compute quantities involved in chemical reactions, written in Rust. The balancer maps stoichiometric equations to matrices and uses Gauss's elimination algorithm, adapted to keep all coefficients integer and minimal.


  "Intelligent" sudoku solver  

Personal project, 2023

Keyword: Automated reasoning, Sudoku, Constraints satisfaction

An "intelligent" sudoku solver, that implements reasoning rules and heuristics to limit the use of backtracking. This solver is written in Rattlesnake, serving as the largest example program for this toy language.



  Language features à-la-carte  

Bachelor project, EPFL Scala center, Spring semester 2022

Keywords: Static code analysis, Program transformation, Scala

The goal of the project was to build a linter for Scala to check that some features of the language are not used (typically it could be used to guarantee that programs are functional). I also worked on a prototype tool that transforms (some) imperative Scala programs into equivalent functional programs, the goal being to help students understand functional programming.


  Deadlines manager  

Team project for the Software development project class, EPFL, Spring semester 2022

Keywords: Android, Kotlin

My teammates and I created Multimatum, an Android app to manage deadlines.