D3.1: Static Code Analysers and Formal Verification Methods (first version)

This deliverable outlines the foundational structure and early implementation of the static code analysis and formal verification framework under Task T3.1. The framework, bundled into the Static Code Analysis Module, employs advanced Machine Learning (ML) and Deep Learning (DL) techniques to improve vulnerability detection accuracy while minimizing false positives across diverse programming environments. Formal verification methods test software against modeled safety properties, validating critical behavioral requirements, especially in concurrent and functional systems. Together with symbolic execution for comprehensive path analysis, these methods culminate in the Static Supply Chain component Guarantee (SSCG), which consolidates all testing efforts into a structured report that integrates into the RESCALE platform as a first step to the creation of a Trusted Bill of Materials (TBOM).