Valentin Aebi

Keywords: Language design, Type system, Compiler, JVM bytecode, Verification, SMT solver

Simple experimental programming language. I initially designed it as a personal project to learn about compilers, and then used it for several experimental projects. Most notably:

• An implementation of gradual object capabilities (as part of my master's thesis)
  [code] [thesis] [language documentation] [example program]


• A program verifier for an earlier version of Rattlesnake (ft. my project teammates)
  [code] [report] [slides]

Research project, EPFL SYSTEMF laboratory, 2023-2024

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

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. The second version consists of a plugin for the Java compiler.
[code] [report]

Keywords: Static analysis, Bug detection, Control-flow analysis, SMT solver, JVM bytecode

A prototype bug detection engine for Java-based languages, written in Kotlin. It uses symbolic execution to detect errors like null dereferences, out-of-bound array accesses, and divisions by zero. 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.
[code]

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.
[code]