Thesis Proposals

The starting point of this project is represented by the idea of designing and implementing a Web-GIS platform aimed at supporting infrastructure asset management. The case study will focus on a new metro line project, which provides a concrete context for the work. The platform is intended to serve as a decision-support tool that can be used throughout the entire life cycle of the assets, from design and construction to operation and maintenance. Its main purpose is to collect, process, and visualize heterogeneous data from multiple technological and non-technological sources. On this basis, the system will compute and monitor fifteen key performance indicators (KPIs) that describe infrastructure performance and sustainability. The work will focus on developing the complete workflow supporting the Web-GIS platform, from multi-source data extraction and ingestion to storage, KPI computation, and web-based visualization. A central database will act as the backbone for organizing heterogeneous inputs (manual data, IFC/BIM, questionnaires, GIS layers, IoT sensors, images, and video), while dedicated processing services will compute and update fourteen KPIs and make results available via APIs for GIS visualization and dashboarding. An essential aspect of the system will be its ability to handle temporal updates. This means that new incoming data should be incorporated into the database and reflected in the recalculation of KPI values, while at the same time maintaining a historical record that enables long-term monitoring and comparative analysis. This functionality is fundamental for capturing the evolution of infrastructure conditions over time. The expected outcome is a working Web-GIS platform prototype integrating data ingestion, database storage, KPI computation, and web-based GIS visualization. The implementation will be demonstrated on a sample set of KPIs, with an extensible architecture enabling the future inclusion of the complete KPI set.

This thesis focuses on the mathematical verification of "jets"—optimized C-language implementations of specific functions within the Simplicity language. The candidate will select a non-trivial cryptographic function, such as jet::bip_0340_verify (Schnorr signatures), and develop a machine-checked proof using a theorem prover like Coq or Lean. The objective is to demonstrate that the optimized jet is functionally equivalent to the verbose Simplicity program specification, ensuring both performance and high-assurance security. Expected Deliverables: ● A complete, machine-checked proof script in Coq or Lean ● Technical documentation outlining the proof strategy and equivalence results