I am a post doctoral researcher at Uppsala University with an interest in formal methods and program analysis techniques for verification and testing purposes. In particular, I design and apply such rigorous knowledge to internet of things devices, operating systems and complex interactive frameworks.
As a part of the aSSIsT project, I am currently a post doctoral researcher at Uppsala University. The project aims at applying novel methods to detect vulnerabilities on Internet of Things (IoT) devices. In particular, we are focussing on designing automatic analysis and testing methods inspired by hybrid fuzzing systems. Together with the combination of formal methods and testing techniques, the project is collaborating with companies, such as Contiki-NG OS.
I contributed to the open-source project selfie at the University of Salzburg in the Computational Systems team headed by Christoph Kirsch. Selfie is a self compiler/emulator/hosting software dedicated to cstar (a tiny subset of C) and written in a single thousand-line long file. This software is a self contained RISC-U (a tiny subset of RISC-V) operating system and lays down a simple but still expressive base. More precisely, I focussed on a project to extend selfie with analysis and verification features following its simplicity and self-reference. The open-source branch monster proposes a symbolic RISC-U emulator to perform a complete and sound numerical analysis on the input binaries. The goal is to apply a numerical analysis on selfie's binaries and be able to retrieve information for optimizing and verifying low-level code.
I worked as an assistant professor at the University of Pierre et Marie Curie - Paris VI, attached to the Institute for Research and Coordination in Acoustics/Music (IRCAM). I defended my Sc.PhD the 11/10/16 and began a project to merge model checking and constraint satisfaction problems with Pierre Talbot. This project aims at implementing a model checker based on the programming language bonsai to ease the modularity and the definitions of model checking strategies. Following the vision of constraint solving problems, we hope to reduce drastically the explosion-state problem usually limiting model checker applications.
My Sc.Phd Model-Based Testing Real-Time and Interactive Music Systems investigates the formal testing of systems timely interacting with humans in musical contexts. Under the supervision of Florent Jacquemard, we designed a formalized testing method based on the Interactive and RealTime Model (IRTM) capable of modeling multiple time units, input/output synchronization and dynamic process creation. An IRTM is a synchronous based model and assumes the synchronous hypothesis of time stamped logical instants. An offline and online frameworks have been formalized and developed to test fully automatically an interactive system from a score respectively using Uppaal tools and a virtual machine interpreting IRTM. Experiments have been successfully deployed to formally test the software Antescofo started by the team Repmus.