Anna Becchi

Postdoctoral Fellow · Formal Verification and Security Lab
Università della Svizzera italiana (USI), Lugano

About

I am a researcher in formal verification, the field that uses mathematical logic to prove that systems behave as intended. I am currently a postdoctoral fellow in Prof. Natasha Sharygina’s Formal Verification and Security Lab at USI in Lugano, Switzerland, where we develop techniques to make software correct and secure. More technically, I focus on improving the trustworthiness and convergence of algorithms for solving Constrained Horn Clauses (CHCs), such as Spacer and Transition Power Abstraction (TPA).

I earned my PhD in Computer Science with distinction in 2025 from FBK and the University of Trento, Italy, advised by Alessandro Cimatti. My thesis (slides) developed abstraction techniques for reverse-engineering relay-based railway interlockings, to validate the software that replaces them.

Constrained Horn Clauses
Certification
Lean
Model-Based Projection
Quantifier Elimination
Polyhedral Abstraction

News

Jan 2027 Artifact Evaluation Co-Chair of VMCAI 2027, Mexico City, co-located with POPL.
Oct 2026 Program Committee member of NSAD 2026 at SPLASH/ISSTA, Oakland.
Jul 2026 My paper PyCHC: a Framework for Certified Horn Solving and CHC-based Design was accepted at CAV’26.
Dec 2025 My paper Syntactically Convex Model-Based Projection for Linear Real Arithmetic was accepted at TACAS’26.

Publications

Also on dblp ↗

2026

PyCHC: a Framework for Certified Horn Solving and CHC-based Design CAVA. Becchi, M. Blicha, R. Otoni, N. Sharygina · GitHub
Syntactically Convex Model-Based Projection for Linear Real Arithmetic TACASA. Becchi, G. Fedyukovich, A. Gurfinkel, L. Nachmanson · GitHub

2025

Abstractions for Reverse Engineering — Validating the Computerization of Relay-Based Railway Interlocking Systems PhD thesisFBK & University of Trento · slides

2024

Testing the Migration from Analog to Software-Based Railway Interlocking Systems CAVA. Becchi, A. Cimatti, G. Scaglione
Abstraction Modulo Stability FMSD journalA. Becchi, A. Cimatti
P-Stable Abstractions of Hybrid Systems SoSyM journalA. Becchi, A. Cimatti, E. Zaffanella

2023

Searching for i-Good Lemmas to Accelerate Safety Model Checking CAVY. Xia, A. Becchi, A. Cimatti, A. Griggio, J. Li, G. Pu
SMT-Based Stability Verification of an Industrial Switched PI Control Systems DSN-WS. Basagiannis, L. Battista, A. Becchi, A. Cimatti, G. Giantamidis, S. Mover, A. Tacchella, S. Tonetta, V. A. Tsachouridis

2022

Abstraction Modulo Stability for Reverse Engineering CAVA. Becchi, A. Cimatti
NORMA: a Tool for the Analysis of Relay-Based Railway Interlocking Systems TACASA. Amendola, A. Becchi, R. Cavada, A. Cimatti, A. Ferrando, L. Pilati, G. Scaglione, A. Tacchella, M. Zamboni

2020

A Model-Based Approach to the Design, Verification and Deployment of Railway Interlocking System ISoLaA. Amendola, A. Becchi, R. Cavada, A. Cimatti, A. Griggio, G. Scaglione, A. Susi, A. Tacchella, M. Tessi
Synthesis of P-Stable Abstractions SEFMA. Becchi, A. Cimatti, E. Zaffanella
PPLite: Zero-Overhead Encoding of NNC Polyhedra Inf. & Comp. journalA. Becchi, E. Zaffanella

2019

Revisiting Polyhedral Analysis for Hybrid Systems Best Paper Award SASA. Becchi, E. Zaffanella

2018

An Efficient Abstract Domain for Not Necessarily Closed Polyhedra SASA. Becchi, E. Zaffanella
A Direct Encoding for NNC Polyhedra CAVA. Becchi, E. Zaffanella

Software

PyCHC Main developer 2025–2026

Open-source tool for certified Horn solving and CHC-based design.

PythonPySMTPaper: CAV ’26
Golem Contributor 2026

Solver for Constrained Horn Clauses, built on OpenSMT.

C++
ConvexQE Main developer 2025

Open-source personal project experimenting with bidirectional model-based projection.

PythonPySMTPaper: TACAS ’26
NORMA Contributor 2020–2025

Tool for graphical modelling and analysis of relay-based railway interlocking systems. I developed the SMT-based optimizations and the automated property extraction.

PythonnuXmvPySMTMathSATPapers: TACAS ’22, CAV ’22, CAV ’24, FMSD ’24
LRA-BDD Main developer 2020–2022

C++ library combining multi-terminal BDDs and convex polyhedra.

C++Papers: CAV ’22, FMSD ’24, PhD thesis
PPLite Contributor 2017–2020

C++ library for the convex polyhedra abstract domain.

C++Papers: CAV ’18, SAS ’18, Inf. & Comp. ’20
PHAVerLite Contributor 2018–2019

C++ verifier for hybrid systems.

C++Paper: SAS ’19

Service

Artifact Evaluation Co-Chair: VMCAI ’27 · Mexico City, co-located with POPL
Program Committee: NSAD ’26
Artifact Evaluation Committee: TACAS ’25–’26 · SAS ’22, ’24 · CAV ’22, ’24, ’26
Subreviewer: FASE ’26 · SMT ’26 · DATE ’25 · FM ’24 · CAV ’20, ’22, ’24 · TACAS ’20–’24, ’27 · ATVA ’21, ’22, ’26 · FMCAD ’22, ’26 · SEFM ’20, ’22 · SETTA ’20
Student Volunteer: CAV ’24 · FMCAD ’22 · FLoC ’18, ’22