Ph.D XL

Supervisor: Alessandro Cimatti, co-supervisor: Stefano Tonetta

Room: FBK, DSIP Unit

Mail: sambrotta.alberto@spes.uniud.it

Research Project

Diagnosing Failures in Runtime Verification

Runtime Verification (RV) is a formal verification technique that analyzes a system's behavior during its execution to ensure compliance with specified properties (e.g., safety, correctness). Unlike static methods such as model checking, RV operates in real-time or post-execution, making it a lightweight approach. It employs software monitors to track system events and verify adherence to temporal logics or formal rules (e.g., LTL, automata). RV is particularly valuable in safety-critical systems (e.g., robotics, IoT), where dynamic errors must be detected immediately to mitigate risks.

Detecting a violation is only the first step. The subsequent challenge lies in pinpointing which components caused the failure, especially in complex systems with multiple interactions. Not all errors detected during monitoring are necessarily linked to the violation: some may be harmless, while others might have indirectly triggered it. Additionally, intermittent malfunctions, concurrency issues, or timing delays complicate isolating root causes. Accurate diagnosis thus requires techniques that differentiate correlation from causation, minimize false positives, and reduce computational overhead.

My research regards the above topics, that is finding root causes of property violation during runtime verification.