Hello there!
I'm a postdoc at Formal Verification and Security Lab at USI, Lugano, Switzerland, working with Prof. Natasha Sharygina on program verification with Constrained Horn Clauses.
In September 2025, I obtained my PhD in Computer Science from Fondazione Bruno Kessler, and University of Trento, under the supervision of Alessandro Cimatti.
My PhD thesis (slides) introduces abstraction techniques for reverse engineering, verification and test case generation for cyber-physical systems described as infinite-state timed transition systems or hybrid systems. We applied the proposed techniques in an industrial project addressing the migration from legacy (electro-mechanical) railway interlocking systems, to their software-based re-implementation.
Research interests
I'm interested in SMT-based invariant checking techniques and their interaction with approaches based on abstract interpretation. In the past, I developed an efficient domain for convex polyhedra, applied to both static analysis and reachability of piecewise constant hybrid systems.
Publications
- [b01]"Abstractions for Reverse Engineering", Anna Becchi — PhD thesis, September 2025
- [c10]"Testing the migration from analog to software-based Railway Interlocking Systems", A. Becchi, A. Cimatti, G. Scaglione — CAV'24
- [j03]"Abstraction Modulo Stability", A. Becchi, A. Cimatti — FMSD'24
- [j02]"P-stable abstractions of hybrid systems", A. Becchi, A. Cimatti, E. Zaffanella — SoSyM'24
- [c09]"Searching for i-Good Lemmas to Accelerate Safety Model Checking", Y. Xia, A. Becchi, A. Cimatti, A. Griggio, J. Li, G. Pu — CAV'23
- [c08]"SMT-Based Stability Verification of an Industrial Switched PI Control Systems", S. Basagiannis, L. Battista, A. Becchi, A. Cimatti, G. Giantamidis, S. Mover, A. Tacchella, S. Tonetta, V. A. Tsachouridis — DSN-W'23
- [c07]"Abstraction Modulo Stability for Reverse Engineering", A. Becchi, A. Cimatti — CAV'22
- [c06]"NORMA: a tool for the analysis of Relay-based Railway Interlocking Systems", A. Amendola, A. Becchi, R. Cavada, A. Cimatti, A. Ferrando, L. Pilati, G. Scaglione, A. Tacchella, M. Zamboni — TACAS'22
- [c05]"A Model-Based Approach to the Design, Verification and Deployment of Railway Interlocking System", A. Amendola, A. Becchi, R. Cavada, A. Cimatti, A. Griggio, G. Scaglione, A. Susi, A. Tacchella, M. Tessi — ISoLa'20
- [c04]"Synthesis of P-Stable Abstractions", A. Becchi, A. Cimatti, E. Zaffanella — SEFM'20: 214–230
- [j01]"PPLite: Zero-overhead encoding of NNC polyhedra", A. Becchi, E. Zaffanella — Inf&Comp'20
- [c03]"Revisiting Polyhedral Analysis for Hybrid Systems", A. Becchi, E. Zaffanella — SAS'19 — Winner of the Radhia Cousot Young Researcher Best Paper Award
- [c02]"An Efficient Abstract Domain for Not Necessarily Closed Polyhedra", A. Becchi, E. Zaffanella — SAS'18
- [c01]"A Direct Encoding for NNC Polyhedra", A. Becchi, E. Zaffanella — CAV'18
Experiences
- Dagstuhl seminar Sound Static Program Analysis in Modern Software Engineering, 2025 October
- International Visiting Graduate Student in University of Waterloo, supervised by Arie Gurfinkel (2024 May - 2024 August)
- Marktoberdorf Summer School Safety and Security through Formal Verification, 2023 August
- Dagstuhl seminar (collector) Theoretical Advances and Emerging Applications in Abstract Interpretation, 2023 July
- Software developer @ Fondazione Bruno Kessler, 2019 September - 2021 October
- Subreviewer: FASE'26, DATE'25, CAV'20-22-24,TACAS'20-21-22-23-24, FM'24, SEFM'20-22, SETTA'20, ATVA'21-22, FMCAD'22
- Artifact Evaluation Committe member: TACAS'25-26, CAV'22-23-24, SAS'22-24
- Conference service volunteer: FLoC'18, FLoC'22, FMCAD'22.