Formal Specification of Beliefs in Multi-Agent Systems. - Massimo Benerecetti; Alessandro Cimatti; Enrico Giunchiglia; Fausto Giunchiglia; Luciano Serafini (ATAL, 1996)

METAFOL: Program tactics and logic tactics plus reflection. - Massimo Benerecetti; Luca Spalazzi (Future Gener. Comput. Syst., 1996)

Formalizing Belief Reports - The Approach and a Case Study. - Massimo Benerecetti; Paolo Bouquet; Chiara Ghidini (AIMSA, 1998)

A Model Checking Algorithm for Multiagent Systems. - Massimo Benerecetti; Fausto Giunchiglia; Luciano Serafini (ATAL, 1998)

Multiagent Systems Verification via Model Checking. - Massimo Benerecetti; Fausto Giunchiglia; Luciano Serafini (EUROVAV, 1998)

Model Checking Multiagent Systems. - Massimo Benerecetti; Fausto Giunchiglia; Luciano Serafini (J. Log. Comput., 1998)

Formal specification of beliefs in multi-agent systems. - Massimo Benerecetti; Enrico Giunchiglia; Luciano Serafini; Adolfo Villafiorita (Int. J. Intell. Syst., 1999)

Model Checking-Based Analysis of Multiagent Systems. - Massimo Benerecetti; Fausto Giunchiglia (FAABS, 2000)

A Logic of Belief and a Model Checking Algorithm for Security Protocols. - Massimo Benerecetti; Fausto Giunchiglia; Maurizio Panti; Luca Spalazzi (FORTE, 2000)

Model Checking Security Protocols Using a Logic of Belief. - Massimo Benerecetti; Fausto Giunchiglia (TACAS, 2000)

Contextual reasoning distilled. - Massimo Benerecetti; Paolo Bouquet; Chiara Ghidini (J. Exp. Theor. Artif. Intell., 2000)

On the Dimensions of Context Dependence: Partiality, Approximation, and Perspective. - Massimo Benerecetti; Paolo Bouquet; Chiara Ghidini (CONTEXT, 2001)

Distributed Context-Aware Systems. - Massimo Benerecetti; Paolo Bouquet; Matteo Bonifacio (Hum. Comput. Interact., 2001)

Validation of Multiagent Systems by Symbolic Model Checking. - Massimo Benerecetti; Alessandro Cimatti (AOSE, 2002)

Verification of Payment Protocols via MultiAgent Model Checking. - Massimo Benerecetti; Maurizio Panti; Luca Spalazzi; Simone Tacconi (CAiSE, 2002)

Verification of the SSL/TLS Protocol Using a Model Checkable Logic of Belief and Time. - Massimo Benerecetti; Maurizio Panti; Luca Spalazzi; Simone Tacconi (SAFECOMP, 2002)

Verification of recursive parallel systems - Laura Bozzelli; Massimo Benerecetti; Adriano Peron (CoRR, 2003)

Soundness of Schema Matching Methods. - Massimo Benerecetti; Paolo Bouquet; Stefano Zanobini (ESWC, 2005)

Model Checking Linear Programs with Arrays. - Alessandro Armando; Massimo Benerecetti; Jacopo Mantovani (SoftMC@CAV, 2005)

The eureka tool for software model checking. - Alessandro Armando; Massimo Benerecetti; Dario Carotenuto; Jacopo Mantovani; Pasquale Spica (ASE, 2007)

Abstraction Refinement of Linear Programs with Arrays. - Alessandro Armando; Massimo Benerecetti; Jacopo Mantovani (TACAS, 2007)

TPMC: A Model Checker For Time-Sensitive Security Protocols. - Massimo Benerecetti; Nicola Cuomo; Adriano Peron (J. Comput., 2009)

Timed protocols insecurity problem is NP-complete. - Massimo Benerecetti; Nicola Cuomo; Adriano Peron (HPCS, 2010)

Analysis of Timed Recursive State Machines. - Massimo Benerecetti; Stefano Minopoli; Adriano Peron (TIME, 2010)

Revisiting synthesis of switching controllers for Linear Hybrid systems. - Massimo Benerecetti; Marco Faella; Stefano Minopoli (CDC/ECC, 2011)

Automatic Synthesis of Switching Controllers for Linear Hybrid Automata - Massimo Benerecetti; Marco Faella; Stefano Minopoli (CoRR, 2011)

Towards Efficient Exact Synthesis for Linear Hybrid Systems - Massimo Benerecetti; Marco Faella; Stefano Minopoli (GandALF, 2011)

Reachability games for linear hybrid systems. - Massimo Benerecetti; Marco Faella; Stefano Minopoli (HSCC, 2012)

Tracking differentiable trajectories across polyhedra boundaries. - Massimo Benerecetti; Marco Faella (HSCC, 2013)

Substructure Temporal Logic. - Massimo Benerecetti; Fabio Mogavero; Aniello Murano (LICS, 2013)

Timed protocol insecurity problem is NP-complete. - Massimo Benerecetti; Adriano Peron (Future Gener. Comput. Syst., 2013)

Automatic synthesis of switching controllers for linear hybrid systems: Safety control. - Massimo Benerecetti; Marco Faella; Stefano Minopoli (Theor. Comput. Sci., 2013)

A Distributed Information Extraction System Integrating Ontological Knowledge and Probabilistic Classifiers. - Anita Alicante; Massimo Benerecetti; Anna Corazza; Stefano Silvestri (3PGCIC, 2014)

Dynamic State Machines for Formalizing Railway Control System Specifications. - Roberto Nardone; Ugo Gentile; Adriano Peron; Massimo Benerecetti; Valeria Vittorini; Stefano Marrone 001; Renato De Guglielmo; Nicola Mazzocca; Luigi Velardi (FTSCS, 2014)

Counterexample-guided abstraction refinement for linear programs with arrays. - Alessandro Armando; Massimo Benerecetti; Jacopo Mantovani (Autom. Softw. Eng., 2014)

Modeling Railway Control Systems in Promela. - Roberto Nardone; Ugo Gentile; Massimo Benerecetti; Adriano Peron; Valeria Vittorini; Stefano Marrone 001; Nicola Mazzocca (FTSCS, 2015)

Reasoning About Substructures and Games. - Massimo Benerecetti; Fabio Mogavero; Aniello Murano (ACM Trans. Comput. Log., 2015)

Improving Priority Promotion for Parity Games. - Massimo Benerecetti; Daniele Dell'Erba; Fabio Mogavero (Haifa Verification Conference, 2016)

A Delayed Promotion Policy for Parity Games. - Massimo Benerecetti; Daniele Dell'Erba; Fabio Mogavero (GandALF, 2016)

A distributed architecture to integrate ontological knowledge into information extraction. - Anita Alicante; Massimo Benerecetti; Anna Corazza; Stefano Silvestri (Int. J. Grid Util. Comput., 2016)

Timed recursive state machines: Expressiveness and complexity. - Massimo Benerecetti; Adriano Peron (Theor. Comput. Sci., 2016)

Robust Exponential Worst Cases for Divide-et-Impera Algorithms for Parity Games. - Massimo Benerecetti; Daniele Dell'Erba; Fabio Mogavero (GandALF, 2017)

Tracking smooth trajectories in linear hybrid systems. - Massimo Benerecetti; Marco Faella (Inf. Comput., 2017)

Dynamic state machines for modelling railway control systems. - Massimo Benerecetti; Renato De Guglielmo; Ugo Gentile; Stefano Marrone 001; Nicola Mazzocca; Roberto Nardone; Adriano Peron; Luigi Velardi; Valeria Vittorini (Sci. Comput. Program., 2017)

Automatic Synthesis of Switching Controllers for Linear Hybrid Systems: Reachability Control. - Massimo Benerecetti; Marco Faella (ACM Trans. Embed. Comput. Syst., 2017)

Solving parity games via priority promotion. - Massimo Benerecetti; Daniele Dell'Erba; Fabio Mogavero (Formal Methods Syst. Des., 2018)

Satisfiability in Strategy Logic Can Be Easier than Model Checking. - Erman Acar; Massimo Benerecetti; Fabio Mogavero (AAAI, 2019)

From Dynamic State Machines to Promela. - Massimo Benerecetti; Ugo Gentile; Stefano Marrone 001; Roberto Nardone; Adriano Peron; Luigi L. L. Starace; Valeria Vittorini (SPIN, 2019)

From Quasi-Dominions to Progress Measures. - Massimo Benerecetti; Daniele Dell'Erba; Marco Faella; Fabio Mogavero (CoRR, 2020)

Robust worst cases for parity games algorithms. - Massimo Benerecetti; Daniele Dell'Erba; Fabio Mogavero (Inf. Comput., 2020)

An OSLC-based environment for system-level functional testing of ERTMS/ETCS controllers. - Roberto Nardone; Stefano Marrone 001; Ugo Gentile; Aniello Amato; Gregorio Barberio; Massimo Benerecetti; Renato De Guglielmo; Beniamino Di Martino; Nicola Mazzocca; Adriano Peron; Gaetano Pisani; Luigi Velardi; et al. (J. Syst. Softw., 2020)

Expressing Structural Temporal Properties of Safety Critical Hierarchical Systems. - Massimo Benerecetti; Fabio Mogavero; Adriano Peron; Luigi Libero Lucio Starace (QUATIC, 2021)

Quantifying Over Trees in Monadic Second-Order Logic. - Massimo Benerecetti; Laura Bozzelli; Fabio Mogavero; Adriano Peron (LICS, 2023)

Good-for-Game QPTL: An Alternating Hodges Semantics. - Dylan Bellier; Massimo Benerecetti; Dario Della Monica; Fabio Mogavero (ACM Trans. Comput. Log., 2023)

Taming Strategy Logic: Non-Recurrent Fragments. - Massimo Benerecetti; Fabio Mogavero; Adriano Peron (Inf. Comput., 2023)

Alternating (In)Dependence-Friendly Logic. - Dylan Bellier; Massimo Benerecetti; Dario Della Monica; Fabio Mogavero (Ann. Pure Appl. Log., 2023)

Plan Logic. - Dylan Bellier; Massimo Benerecetti; Fabio Mogavero; Sophie Pinchinat (FSTTCS, 2024)

Automata-Theoretic Characterisations of Branching-Time Temporal Logics. - Massimo Benerecetti; Laura Bozzelli; Fabio Mogavero; Adriano Peron (ICALP, 2024)

Full Characterisation of Extended CTL. - Massimo Benerecetti; Laura Bozzelli; Fabio Mogavero; Adriano Peron (TIME, 2024)

Model Checking Linear Temporal Properties on Polyhedral Systems. - Massimo Benerecetti; Marco Faella; Fabio Mogavero (TIME, 2024)

Solving mean-payoff games via quasi dominions. - Massimo Benerecetti; Daniele Dell'Erba; Fabio Mogavero (Inf. Comput., 2024)

Priority Promotion with Parysian flair. - Massimo Benerecetti; Daniele Dell'Erba; Fabio Mogavero; Sven Schewe; Dominik Wojtczak (J. Comput. Syst. Sci., 2025)