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

Biochemically-Informed Neural Networks

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

Fact-Fortress

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.

Pacti

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

Sym-CPS

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

CROME

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

Crome-Contracts

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

Crome-Logic

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

Crome-Synthesis

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

Cogomo

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

WiseML

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

Movemo

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

Search and Rescue Challenge

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

NASA DAIDALUS

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

CHI+MED Integrated Clinical Environment

Communication middleware enabling co-simulation of device prototypes, facilitating interoperability with medical devices represented as mathematical models (using PVS).