Hi there!
I'm a Computer Science PhD student in the Formal Methods unit of Fondazione Bruno Kessler and University of Trento (Italy), supervised by Alessandro Cimatti.
Research interests
My PhD topic is automated formal verification of infinite-state transition systems. I am working on an industrial project addressing the migration from analog legacy Railway Interlocking Systems to their software-based re-implementation, tackling reverse engineering, verification, and automated test case generation from electro-mechanical circuits.
I'm also 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.
Selected publications
- "Testing the migration from analog to software-based Railway Interlocking Systems", A. Becchi, A. Cimatti, G. Scaglione -- CAV'24
- "Abstraction Modulo Stability", A. Becchi, A. Cimatti -- FMSD'24
- "P-stable abstractions of hybrid systems", A. Becchi, A. Cimatti, E. Zaffanella -- SoSyM'24
- "Searching for i-Good Lemmas to Accelerate Safety Model Checking", Y. Xia, A. Becchi, A. Cimatti, A. Griggio, J. Li, G. Pu -- CAV'23
- "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
- "Abstraction Modulo Stability for Reverse Engineering", A. Becchi, A. Cimatti -- CAV'22
- "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
- "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
- "PPLite: Zero-overhead encoding of NNC polyhedra", A. Becchi, E. Zaffanella -- Inf&Comp'20
- "Revisiting Polyhedral Analysis for Hybrid Systems", A. Becchi, E. Zaffanella -- SAS'19 -- Winner of Radhia Cousot Young Researcher Best Paper Award
- "An Efficient Abstract Domain for Not Necessarily Closed Polyhedra ", A. Becchi, E. Zaffanella -- SAS'18
- "A Direct Encoding for NNC Polyhedra", A. Becchi, E. Zaffanella -- CAV'18
Experiences
- 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 Theoretical Advances and Emerging Applications in Abstract Interpretation, 2023 July
- Software developer @ Fondazione Bruno Kessler, 2019 September - 2021 October
- Subreviewer: TACAS'20-21-22-23-24, CAV'20-22-24, SEFM'20-22, SETTA'20, ATVA'21-22, FMCAD'22
- Artifact Evaluation Committe member: TACAS'25, CAV'22-23-24, SAS'22-24
- Conference service volunteer: FLoC'18, FLoC'22, FMCAD'22.