USI - Email

Archive / INF Seminars / INF_2025_05_26_AnnaBecchi

USI - Email

	Abstraction Modulo Stability for reverse engineering cyber-physical systems

Host: Prof. Natasha Sharygina

Monday

26.05

USI Campus EST, Room C1.03

14:00 - 15:00


	Anna Becchi Fondazione Bruno Kessler, Trento

Abstract: The Italian Railway Network (RFI), together with Fondazione Bruno Kessler, is addressing the migration from analog interlockings to a newly developed software control. The absence of formal specifications for the trusted legacy implementation challenges this transition. To support the reverse-engineering of cyber-physical systems, we have developed Abstraction Modulo Stability (AMS), a general framework that captures the run-to-completion transactions triggered by inputs while abstracting away transient states. AMS allows the extraction of high-level properties and the generation of test cases directly from the analog implementation. In the context of the Italian interlockings, this methodology has been proven effective in finding bugs in the new software. The talk concludes with a recent contribution related to the quantifier elimination (QE) problem. We introduce a novel extension of the Model-Based Projection concept, which improves efficiency and conciseness of QE and enables new strategies in the many clients of QE, including CHC solvers.

Biography: Anna Becchi is a Computer Science PhD candidate at Fondazione Bruno Kessler in Trento, Italy, focusing on reverse engineering and verification of cyber-physical systems in collaboration with the Italian Railway Network. Her past work involved abstract interpretation in the domain of convex polyhedra, applied to both static analysis and hybrid systems verification. Her current research interests include SMT-based invariant checking and CHC solving.