Poliac is an LLM-based framework designed to assist DevOps engineers in improving Infrastructure as Code (IaC) configurations. It combines IaC artifacts, requirements expressed in natural language, and operational data collected from the deployed system to generate infrastructure recommendations grounded in runtime behavior. By incorporating metrics such as CPU, memory, latency, and throughput, Poliac helps reduce ambiguity in LLM-generated recommendations and avoid unnecessary resource provisioning.
Scopeannon is an OCaml-based static analyzer designed to help developers understand Ansible’s unusual variable scoping rules. It analyzes Ansible playbooks to determine which scopes are consulted when variables are resolved, making precedence rules and hidden interactions between scopes explicit. Scopeannon produces an augmented playbook that highlights potential unexpected scope selections and unintended variable overrides.
Ballet was developed during my first postdoc to tackle the challenges faced by cross-functional DevOps teams in Edge Computing and Cyber-Physical Systems. Ballet is a fast, decentralized tool that automates choreographies for cross-DevOps reconfigurations. Each node handles its own coordination, planning, and execution, making reconfiguration seamless. Ballet's planner uses constraint programming to infer a local reconfiguration plan. However, such a plan often has consequences on depending services. Then, using a gossip protocole alongside a consensus algorithm, these consequences are formalized as constraints and propagated through the network. The execution phase of Ballet decentralizes Concerto, ensuring efficient and reliable reconfigurations across distributed systems.
SparkTE stands as a significant milestone in my Ph.D. contribution, providing a certified distributed solution for model transformation engines. Developed as a scalable distributed implementation of the CoqTL specification, SparkTE offers a versatile platform for formal reasoning and certification of model transformations. Unlike traditional approaches that prioritize certification at the expense of performance, SparkTE introduces an additional feature: a customizable engine. This aspect allows users to explore various design choices, striking the perfect balance between certification requirements and execution efficiency. With SparkTE, researchers and practitioners gain a flexible and efficient tool for navigating the complexities of model transformations with confidence.
PySke, an academic project initiated during my master's degree, is an algorithmic skeleton library for Python designed to simplify programming for shared or distributed memory parallel architectures. My contribution involved creating PySke's skeletal parallel programming patterns, particularly focusing on skeletons for lists and trees. Additionally, I contributed in the design of a lazy mechanism in PySke's execution, facilitating performance enhancement through equivalence rewriting of composition to optimize the composition of skeletons.
SyDPaCC is a collection of libraries for the Coq proof assistant enabling the transformation of high-complexity functional programs into more efficient versions, which can be parallelized and extracted into OCaml code with calls to the BSML library. During my master's degree, I contributed to SyDPaCC by formalizing map and reduce skeletons on binary trees and partially proving their correctness, enhancing the library's functionality for parallel computing.