Integrated Modeling and Verification of Real-Time Systems through Multiple Paradigms. - Marcello M. Bersani; Carlo A. Furia; Matteo Pradella; Matteo Rossi 001 (SEFM, 2009)

SMT-based Verification of LTL Specification with Integer Constraints and its Application to Runtime Checking of Service Substitutability. - Marcello M. Bersani; Luca Cavallaro; Achille Frigeri; Matteo Pradella; Matteo Rossi 001 (SEFM, 2010)

Bounded Reachability for Temporal Logic over Constraint Systems. - Marcello M. Bersani; Achille Frigeri; Angelo Morzenti; Matteo Pradella; Matteo Rossi 001; Pierluigi San Pietro (TIME, 2010)

SMT-based Verification of LTL Specifications with Integer Constraints and its Application to Runtime Checking of Service Substitutability - Marcello M. Bersani; Luca Cavallaro; Achille Frigeri; Matteo Pradella; Matteo Rossi 001 (CoRR, 2010)

The Complexity of Reversal-Bounded Model-Checking. - Marcello M. Bersani; Stéphane Demri (FroCoS, 2011)

On Some Classes of 2D Languages and Their Relations. - Marcello M. Bersani; Achille Frigeri; Alessandra Cherubini (IWCIA, 2011)

Completeness of the Bounded Satisfiability Problem for Constraint LTL. - Marcello M. Bersani; Achille Frigeri; Matteo Rossi 001; Pierluigi San Pietro (RP, 2011)

Bounded approaches for verification of infinite-state systems. - Marcello M. Bersani (2012)

Deciding Continuous-Time Metric Temporal Logic with Counting Modalities. - Marcello M. Bersani; Matteo Rossi 001; Pierluigi San Pietro (RP, 2013)

A Tool for Deciding the Satisfiability of Continuous-Time Metric Temporal Logic. - Marcello M. Bersani; Matteo Rossi 001; Pierluigi San Pietro (TIME, 2013)

Deciding the Satisfiability of MITL Specifications. - Marcello Maria Bersani; Matteo Rossi 001; Pierluigi San Pietro (GandALF, 2013)

On the Satisfiability of Metric Temporal Logics over the Reals. - Marcello Maria Bersani; Matteo Rossi 001; Pierluigi San Pietro (Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2013)

Expressiveness and complexity of regular pure two-dimensional context-free languages. - Marcello M. Bersani; Achille Frigeri; Alessandra Cherubini (Int. J. Comput. Math., 2013)

SMT-Based Checking of SOLOIST over Sparse Traces. - Marcello Maria Bersani; Domenico Bianculli; Carlo Ghezzi; Srdan Krstic; Pierluigi San Pietro (FASE, 2014)

Towards the formalization of properties of cloud-based elastic systems. - Marcello M. Bersani; Domenico Bianculli; Schahram Dustdar; Alessio Gambi; Carlo Ghezzi; Srdan Krstic (PESOS, 2014)

A Timed Semantics of Workflows. - Marcello M. Bersani; Salvatore Distefano; Luca Ferrucci; Manuel Mazzara (ICSOFT (Selected Papers), 2014)

An LTL Semantics of BusinessWorkflows with Recovery. - Luca Ferrucci; Marcello M. Bersani; Manuel Mazzara (ICSOFT PT, 2014)

A Logical Characterization of Timed (non-)Regular Languages. - Marcello M. Bersani; Matteo Rossi 001; Pierluigi San Pietro (MFCS (1), 2014)

An LTL Semantics of Business Workflows with Recovery. - Luca Ferrucci; Marcello M. Bersani; Manuel Mazzara (CoRR, 2014)

Constraint LTL satisfiability checking without automata. - Marcello M. Bersani; Achille Frigeri; Angelo Morzenti; Matteo Pradella; Matteo Rossi 001; Pierluigi San Pietro (J. Appl. Log., 2014)

An SMT-based approach to satisfiability checking of MITL. - Marcello M. Bersani; Matteo Rossi 001; Pierluigi San Pietro (Inf. Comput., 2015)

The Cost of Formal Verification in Adaptive CPS. An Example of a Virtualized Server Node. - Marcello M. Bersani; Marisol García-Valls (HASE, 2016)

Towards the Formal Verification of Data-Intensive Applications Through Metric Temporal Logic. - Francesco Marconi; Marcello M. Bersani; Madalina Erascu; Matteo Rossi 001 (ICFEM, 2016)

Efficient large-scale trace checking using mapreduce. - Marcello M. Bersani; Domenico Bianculli; Carlo Ghezzi; Srdan Krstic; Pierluigi San Pietro (ICSE, 2016)

A tool for verification of big-data applications. - Marcello M. Bersani; Francesco Marconi; Matteo Rossi 001; Madalina Erascu (QUDOS@ISSTA, 2016)

Continuous Architecting of Stream-Based Systems. - Marcello M. Bersani; Francesco Marconi; Damian A. Tamburri; Pooyan Jamshidi; Andrea Nodari (WICSA, 2016)

Formal verification of storm topologies through D-VerT. - Francesco Marconi; Marcello M. Bersani; Matteo Rossi 001 (SAC, 2017)

Formal verification of data-intensive applications through model checking modulo theories. - Marcello M. Bersani; Francesco Marconi; Matteo Rossi 001; Madalina Erascu; Silvio Ghilardi (SPIN, 2017)

Towards DevOps for Privacy-by-Design in Data-Intensive Applications: A Research Roadmap. - Michele Guerriero; Damian A. Tamburri; Youssef Ridene; Francesco Marconi; Marcello M. Bersani; Matej Artac (ICPE Companion, 2017)

A logical characterization of timed regular languages. - Marcello M. Bersani; Matteo Rossi 001; Pierluigi San Pietro (Theor. Comput. Sci., 2017)

DevOps Service Observability By-Design: Experimenting with Model-View-Controller. - Damian A. Tamburri; Marcello M. Bersani; Raffaela Mirandola; Giorgio Pea (ESOCC, 2018)

On the Timed Analysis of Big-Data Applications. - Francesco Marconi; Giovanni Quattrocchi; Luciano Baresi; Marcello M. Bersani; Matteo Rossi 001 (NFM, 2018)

Trace Checking of Streaming Applications through DICE-TraCT. - Marcello M. Bersani; Francesco Marconi; Matteo Rossi 001 (ICPE Companion, 2018)

A Flexible Approach for Checking Timed Automata on Continuous Time Semantics. - Claudio Menghi; Marcello M. Bersani; Matteo Rossi 001; Pierluigi San Pietro (CoRR, 2018)

Online verification in cyber-physical systems: Practical bounds for meaningful temporal costs. - Marcello M. Bersani; Marisol García-Valls (J. Softw. Evol. Process., 2018)

Teaching Formal Methods: An Experience Report. - Mehrnoosh Askarpour; Marcello M. Bersani (FISEE, 2019)

Verifying big data topologies by-design : a semi-automated approach. - Marcello M. Bersani; Francesco Marconi; Damian A. Tamburri; Andrea Nodari; Pooyan Jamshidi (J. Big Data, 2019)

Mind the gap: Robotic Mission Planning Meets Software Engineering. - Mehrnoosh Askarpour; Claudio Menghi; Gabriele Belli; Marcello M. Bersani; Patrizio Pelliccione (FormaliSE@ICSE, 2020)

Formal Verification of Human-Robot Interaction in Healthcare Scenarios. - Livia Lestingi; Mehrnoosh Askarpour; Marcello M. Bersani; Matteo Rossi 001 (SEFM, 2020)

A Model-driven Approach for the Formal Analysis of Human-Robot Interaction Scenarios. - Livia Lestingi; Mehrnoosh Askarpour; Marcello M. Bersani; Matteo Rossi 001 (SMC, 2020)

Statistical Model Checking of Human-Robot Interaction Scenarios. - Livia Lestingi; Mehrnoosh Askarpour; Marcello M. Bersani; Matteo Rossi 001 (AREA@ECAI, 2020)

Using formal verification to evaluate the execution time of Spark applications. - Luciano Baresi; Marcello M. Bersani; Francesco Marconi; Giovanni Quattrocchi; Matteo Rossi 001 (Formal Aspects Comput., 2020)

PuRSUE -from specification of robotic environments to synthesis of controllers. - Marcello M. Bersani; Matteo Soldo; Claudio Menghi; Patrizio Pelliccione; Matteo Rossi 001 (Formal Aspects Comput., 2020)

On the initialization of clocks in timed formalisms. - Marcello M. Bersani; Matteo Rossi 001; Pierluigi San Pietro (Theor. Comput. Sci., 2020)

Model Checking MITL Formulae on Timed Automata: A Logic-based Approach. - Claudio Menghi; Marcello M. Bersani; Matteo Rossi 001; Pierluigi San Pietro (ACM Trans. Comput. Log., 2020)

Improved Bounded Model Checking of Timed Automata. - Robert L. Smith; Marcello M. Bersani; Matteo Rossi 001; Pierluigi San Pietro (FormaliSE@ICSE, 2021)

RoboMAX: Robotic Mission Adaptation eXemplars. - Mehrnoosh Askarpour; Christos Tsigkanos; Claudio Menghi; Radu Calinescu; Patrizio Pelliccione; Sergio García 002; Ricardo Caldas; Tim J. von Oertzen; Manuel Wimmer; Luca Berardinelli; Matteo Rossi 001; Marcello M. Bersani; et al. (SEAMS@ICSE, 2021)

Edge-Based Runtime Verification for the Internet of Things. - Christos Tsigkanos; Marcello M. Bersani; Pantelis A. Frangoudis; Schahram Dustdar (SERVICES, 2021)

A Deployment Framework for Formally Verified Human-Robot Interactions. - Livia Lestingi; Mehrnoosh Askarpour; Marcello M. Bersani; Matteo Rossi 001 (IEEE Access, 2021)

Engineering of Trust Analysis-Driven Digital Twins for a Medical Device. - Marcello M. Bersani; Chiara Braghin; Angelo Gargantini; Raffaela Mirandola; Elvinia Riccobene; Patrizia Scandurra (ECSA (Tracks and Workshops), 2022)

Towards Trust-preserving Continuous Co-evolution of Digital Twins. - Marcello M. Bersani; Chiara Braghin; Vittorio Cortellessa; Angelo Gargantini; Vincenzo Grassi; F. Lo Presti; Raffaela Mirandola; Alfonso Pierantonio; Elvinia Riccobene; Patrizia Scandurra (ICSA Companion, 2022)

Formal Modeling and Verification of Multi-Robot Interactive Scenarios in Service Settings. - Livia Lestingi; Cristian Sbrolli; Pasquale Scarmozzino; Giorgio Romeo; Marcello M. Bersani; Matteo Rossi 001 (FormaliSE@ICSE, 2022)

Model-Driven Development of Service Robot Applications Dealing With Uncertain Human Behavior. - Livia Lestingi; Marcello M. Bersani; Matteo Rossi 001 (IEEE Intell. Syst., 2022)

Event-sourced, observable software architectures: An experience report. - Francesco Alongi; Marcello M. Bersani; Nicolò Ghielmetti; Raffaela Mirandola; Damian A. Tamburri (Softw. Pract. Exp., 2022)

Architecting Explainable Service Robots. - Marcello M. Bersani; Matteo Camilli; Livia Lestingi; Raffaela Mirandola; Matteo G. Rossi; Patrizia Scandurra (ECSA, 2023)

Towards Better Trust in Human-Machine Teaming through Explainable Dependability. - Marcello M. Bersani; Matteo Camilli; Livia Lestingi; Raffaela Mirandola; Matteo G. Rossi; Patrizia Scandurra (ICSA-C, 2023)

Explainable Human-Machine Teaming using Model Checking and Interpretable Machine Learning. - Marcello M. Bersani; Matteo Camilli; Livia Lestingi; Raffaela Mirandola; Matteo G. Rossi (FormaliSE, 2023)

A Conceptual Framework for Explainability Requirements in Software-Intensive Systems. - Marcello M. Bersani; Matteo Camilli; Livia Lestingi; Raffaela Mirandola; Matteo G. Rossi; Patrizia Scandurra (REW, 2023)

Specification, stochastic modeling and analysis of interactive service robotic applications. - Livia Lestingi; Davide Zerla; Marcello M. Bersani; Matteo Rossi 001 (Robotics Auton. Syst., 2023)

Analyzing the impact of human errors on interactive service robotic scenarios via formal verification. - Livia Lestingi; Andrea Manglaviti; Davide Marinaro; Luca Marinello; Mehrnoosh Askarpour; Marcello M. Bersani; Matteo Rossi 001 (Softw. Syst. Model., 2024)

Data-Driven Energy Modeling of Machining Centers Through Automata Learning. - Livia Lestingi; Nicla Frigerio; Marcello M. Bersani; Andrea Matta; Matteo G. Rossi (IEEE Trans Autom. Sci. Eng., 2025)

On Decidability Timed Automata with 2 Parametric Clocks. - Marcello M. Bersani; Matteo G. Rossi; Pierluigi San Pietro (CoRR, 2025)

Proactive self-adaptation and assurance of explainable Human-Machine Teaming. - Livia Lestingi; Marcello M. Bersani; Matteo Camilli; Raffaela Mirandola; Matteo G. Rossi; Patrizia Scandurra (J. Syst. Softw., 2026)