Formal Verification of Diagnosability via Symbolic Model Checking. - Alessandro Cimatti; Charles Pecheur; Roberto Cavada (IJCAI, 2003)

Formal analysis of hardware requirements. - Ingo Pill; Simone Semprini; Roberto Cavada; Marco Roveri; Roderick Bloem; Alessandro Cimatti (DAC, 2006)

RAT: A Tool for the Formal Analysis of Requirements. - Roderick Bloem; Roberto Cavada; Ingo Pill; Marco Roveri; Andrei Tchaltsev (CAV, 2007)

Computing Predicate Abstractions by Integrating BDDs and SMT Solvers. - Roberto Cavada; Alessandro Cimatti; Anders Franzén; Krishnamani Kalyanasundaram; Marco Roveri; R. K. Shyamasundar (FMCAD, 2007)

Supporting Requirements Validation: The EuRailCheck Tool. - Roberto Cavada; Alessandro Cimatti; Alessandro Mariotti; Cristian Mattarei; Andrea Micheli; Sergio Mover; Marco Pensallorto; Marco Roveri; Angelo Susi; Stefano Tonetta (ASE, 2009)

OthelloPlay: a plug-in based tool for requirement formalization and validation. - Roberto Cavada; Alessandro Cimatti; Andrea Micheli; Marco Roveri; Angelo Susi; Stefano Tonetta (TOPI@ICSE, 2011)

The nuXmv Symbolic Model Checker. - Roberto Cavada; Alessandro Cimatti; Michele Dorigatti; Alberto Griggio; Alessandro Mariotti; Andrea Micheli; Sergio Mover; Marco Roveri; Stefano Tonetta (CAV, 2014)

Model-Based Design of an Energy-System Embedded Controller Using Taste. - Roberto Cavada; Alessandro Cimatti; Luigi Crema; Mattia Roccabruna; Stefano Tonetta (FM, 2016)

The xSAP Safety Analysis Platform. - Benjamin Bittner; Marco Bozzano; Roberto Cavada; Alessandro Cimatti; Marco Gario; Alberto Griggio; Cristian Mattarei; Andrea Micheli; Gianni Zampedri (TACAS, 2016)

Analysis of Relay Interlocking Systems via SMT-based Model Checking of Switched Multi-Domain Kirchhoff Networks. - Roberto Cavada; Alessandro Cimatti; Sergio Mover; Mirko Sessa; Giuseppe Cadavero; Giuseppe Scaglione (FMCAD, 2018)

A Model-Based Approach to the Design, Verification and Deployment of Railway Interlocking System. - Arturo Amendola; Anna Becchi; Roberto Cavada; Alessandro Cimatti; Alberto Griggio; Giuseppe Scaglione; Angelo Susi; Alberto Tacchella; Matteo Tessi (ISoLA (3), 2020)

COMPASTA: Extending TASTE with Formal Design and Verification Functionality. - Alberto Bombardelli; Marco Bozzano; Roberto Cavada; Alessandro Cimatti; Alberto Griggio; Massimo Nazaria; Edoardo Nicolodi; Stefano Tonetta (IMBSA, 2022)

A Formal IDE for Railways: Research Challenges. - Roberto Cavada; Alessandro Cimatti; Alberto Griggio; Angelo Susi (SEFM Workshops, 2022)

NORMA: a tool for the analysis of Relay-based Railway Interlocking Systems. - Arturo Amendola; Anna Becchi; Roberto Cavada; Alessandro Cimatti; Andrea Ferrando; Lorenzo Pilati; Giuseppe Scaglione; Alberto Tacchella; Marco Zamboni (TACAS (1), 2022)

Reconstructing the High-Level Structure of Legacy Code via Software Model Checking: An Experience Report. - Roberto Cavada; Alessandro Cimatti; Alberto Griggio; Stefano Tonetta; Federico Bonafini; Matteo Campidelli; Andrea Zasa (FMICS, 2024)

A Switching Event-Triggered Model Predictive Control for HVAC Systems. - Mojtaba Sharifzadeh; Hani Beirami; Federico Bonafini; Matteo Campidelli; Roberto Cavada; Alessandro Cimatti; Stefano Tonetta (ICINCO (1), 2024)

Towards the Formal Analysis of Algorithmic Requirements. - Lorenzo Cappelletti; Roberto Cavada; Alessandro Cimatti; Marco Keppel (ISoLA (3), 2024)

Automated Parameterized Verification of a Railway Protection System with Dafny. - Roberto Cavada; Alessandro Cimatti; Alberto Griggio; Christian Lidström; Gianluca Redondi; Giuseppe Scaglione; Matteo Tessi; Dylan Trenti (CAV (4), 2025)

A Specification-Driven Approach to Embedded FDIR Code Generation. - Federico Bonafini; Roberto Cavada; Alessandro Cimatti; Guillermo Gomez; Stefano Tonetta (FMICS, 2025)