Resume
Experience
Software Developer in Formal Methods Unit
Fondazione Bruno Kessler | Trento, Italy | Feb 2024 - Dec 2025
I worked as a software developer in the Formal Methods unit. As a software developer I was tasked with implementing specifications agreed with and set by researchers. More specifically I worked in the context of the ESA funded ExploDTwin 1 project where we designed a framework for digital twins leveraging SysML v2 and model checking tools. The framework, given a SysML v2 formal model, can extract automatically the monitoring and planning component.
In the context of this project I created the initial set of rules and libraries to design a formal model via the SysML v2 modeling language. Afterwards, I designed the monitoring component, which receives telemetries from the real asset and outputs whether the real asset is behaving according to a plan.
During the project I had the chance to improve and develop features for the core suite of tools of the unit, namely NuRV 2.
Technologies: C, Python, Docker, SysML v2, Gitlab CI.
Software Developer in Test
Ifin Sistemi | Padova, Italy | Jun - Aug 2021
This is an internship, part of the curricular activities of my Bachelors. Here, I worked as a software developer in QA. I was tasked with improving the test coverage of the tool Invoice Channel ® (for storage and digitalization of invoices), which I did, by 5%. At the time it was already an established product with millions of lines of code. Moreover, I improved the execution time of the selenium integration pipeline by 50%.
Tecnologies: Java Enterprise, Java 8, JUnit, Mockito.
Education
Master of Science in Computer Science
University of Padova | Padova, Italy | Oct 2021 – Dec 2023
My major consisted of theoretical classes such as formal methods, type theory and software verification. I also specialized in distributed systems, and built a number of project throughout these two years.
- Thesis title: A Local Algorithm for Systems of Fixpoint Equations: Study and Implementation. 3
- Thesis project: github.com/strang3nt/LCSFE
Bachelor of Science in Computer Science
University of Padova | Padova, Italy | Oct 2018 - Sept 2021
These three years I went through the typical computer science classes, such as algorithms, software engineering, networking, web development, and so on. The curriculum is designed to provide hands-on experience and produce engineers that can work with latest technologies and tools out-of-the-gate.
Projects
Telegraft
github.com/strang3nt/Telegraft
Telegraft is a university project whose goal is study the Raft consensus algorithm: it is a simple distributed and replicated chat application which supports the Raft protocol. Telegraft uses Scala and relies heavily on Akka’s technologies.
LCSFE (Local Checking for Systems of Fixpoint Equations)
This project implements a game-theoretical algorithm for providing local solutions of systems of fixpoint equations, under some assumptions of the input. In other words, the goal is to find the greatest or least value (fixpoint equations) of a variable (local solutions), under constraints (the system of equations). This is a very generic and abstract framework, that can be specified to less abstract (but still very abstract 😬) applications.
This is a Rust project, the goal was to provide a modular and performant system. Making it easy to customize the algorithm to different use cases. Use cases are for example solving parity games, or verifying Linear Temporal Equations.
TSP (Travelling Salesperson Problem)
github.com/strang3nt/MeMoCo_assignments
A company produces boards with holes used to build electric panels. The company wants to minimize the total drilling time for each board, taking into account that the time needed for making an hole is the same and constant for all the holes. This is an instance of the Traveling Salesperson Problem (TSP). The project takes as input a graph, and returns either a perfect solution or a “good enough” solution. This is a C++ project, that implement the Travelling Salesperson Problem (TSP) using first an integer linear programming approach, via the IBM ILOG library, and then the Lin-Kernighan heuristic.