Anna Becchi

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

About

I work on program verification with Constrained Horn Clauses (CHCs) in the Formal Verification and Security Lab led by Prof. Natasha Sharygina: my focus is certified Horn solving, model-based projection, and improving the convergence of CHC solving algorithms such as Spacer (PDR) and Transition Power Abstraction.

I received my PhD in Computer Science, with distinction, from FBK and the University of Trento in 2025, advised by Alessandro Cimatti. My thesis (slides) develops abstraction techniques for the reverse engineering of timed and hybrid systems, applied to validating the migration of railway interlockings from relay-based to software-based systems.

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 based on the OpenSMT solver.

C++
ConvexQE Main developer 2025

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

PythonPySMTPaper: TACAS ’26
NORMA Contributor 2020–2025

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