Projects
A selection of projects that I have developed and that are available open-source.
Biochemically-Informed Neural Networks
Configurable Neural Networks with Biochemically-Informed Data Generation
TensorFlow-based framework for neural networks, emphasizing customizable designs, dynamic synthetic data generation rooted in biochemical models, and seamless integration with high-performance computing for enhanced efficiency and scalability.
Fact-Fortress
On-Chain Zero-Knowledge Proof Solution to Fact-Checking
Bockchain-based framework that uses Zero-Knowledge Proofs (ZKP) for trustworthy and private fact-checking leveraging on proof of data provenance, auditable data-access policies and democratizing the construction of ZKP circuits.
Pacti
Open-source Python package for carrying out compositional system analysis and design.
Contributed to PACTI development, an open-source tool for scalable system analysis using Assume-Guarantee contracts with polyhedral constraints. Conducted UAV topology study with contract-based design enforcing context-free grammar rules for feasible topologies.
Sym-CPS
Symbiotic Design for Cyber-Physical Systems
Developed software infrastructure to design, model, and optimize Cyber-Physical Systems (UAVs) at multiple levels of abstraction, including topology, component selection, parameter optimization, and control.
CROME
Contract-Based Robotic Mission Specification
This tool enables designers to model and deploy robotic missions using contracts, allowing them to define the environment and goals using LTL or Specification Patterns. The tool then analyzes the goals, builds a CGG (contract graph), and creates the controllers via reactive synthesis, allowing designers to simulate and test the robotic mission.
Crome-Contracts
Contracts Manipulation Tool
Implemented contract algebra operations for expressing behaviors in Linear Temporal Logic. Currently developing a new web-based version of the tool that supports multiple formalisms in the contracts and greatly simplifies the system specification process.
Crome-Logic
Linear Temporal Logic manipulation library
The tool enables the mapping of LTL formulas to boolean formulas in CNF/DNF and their subsequent simplification using heuristic logic minimization techniques.
Crome-Synthesis
Controllers Synthesis and Manipulation Tool
The tool is capable of breaking down an LTL formula into conjunctions of independent formulas, synthesizing them concurrently into Mealy machines, and running the Mealy machine in parallel, even in the presence of multiple "fix points".
Cogomo
Requirement Engineering Tool
Tool for formally analyzing and refining requirements of component libraries, featuring conflict and incompleteness detection, as well as a greedy optimization algorithm for mapping specifications to components in a library.
WiseML
Runtime monitoring tool for Safe reinforcement learning
Tool for safe and efficient model-free reinforcement learning (RL) in unknown environments. It uses runtime monitoring with a set of monitors to prevent unsafe actions and provide feedback to the agent, which enables the agent to learn faster and achieve the goal efficiently. The approach has been evaluated in randomly generated learning environments and has shown to prevent dangerous actions and improve the agent's performance.
Movemo
Engineering of Reward Functions for reinforcement learning agents
Tool for formally expressing and verifying reward functions in structured state machines, enhancing the design and formal verification of reward functions in reinforcement learning.
Search and Rescue Challenge
Part of the WASP Autonomous System Program
Designed and implemented the complete software stack (Motion Planner, SLAM, Computer Vision, Control) for a cooperative search and rescue mission involving a drone and a land robot (turtlebot).
NASA DAIDALUS
NextGen collision avoidance system Simulator using Formal verification
Flight simulator showcasing NASA Langley's NextGen collision avoidance system (DAIDALUS), incorporating PVS verification for mathematical model execution.
CHI+MED Integrated Clinical Environment
Reverse Engineering of Medical Devices to a formal model
Communication middleware enabling co-simulation of device prototypes, facilitating interoperability with medical devices represented as mathematical models (using PVS).