default search action
Marcello M. Bersani
Person information
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
2020 – today
- 2024
- [j18]Livia Lestingi
, Andrea Manglaviti, Davide Marinaro, Luca Marinello, Mehrnoosh Askarpour, Marcello M. Bersani, Matteo Rossi:
Analyzing the impact of human errors on interactive service robotic scenarios via formal verification. Softw. Syst. Model. 23(2): 473-502 (2024) - 2023
- [j17]Livia Lestingi
Specification, stochastic modeling and analysis of interactive service robotic applications. Robotics Auton. Syst. 163: 104387 (2023) - [c40]Marcello M. Bersani, Matteo Camilli
Architecting Explainable Service Robots. ECSA 2023: 153-169 - [c39]Marcello M. Bersani, Matteo Camilli
Towards Better Trust in Human-Machine Teaming through Explainable Dependability. ICSA-C 2023: 86-90 - [c38]Marcello M. Bersani, Matteo Camilli
Explainable Human-Machine Teaming using Model Checking and Interpretable Machine Learning. FormaliSE 2023: 18-28 - [c37]Marcello M. Bersani, Matteo Camilli
A Conceptual Framework for Explainability Requirements in Software-Intensive Systems. REW 2023: 309-315 - 2022
- [j16]Livia Lestingi
Model-Driven Development of Service Robot Applications Dealing With Uncertain Human Behavior. IEEE Intell. Syst. 37(6): 48-56 (2022) - [j15]Francesco Alongi, Marcello M. Bersani, Nicolò Ghielmetti, Raffaela Mirandola, Damian A. Tamburri
Event-sourced, observable software architectures: An experience report. Softw. Pract. Exp. 52(10): 2127-2151 (2022) - [j14]Christos Tsigkanos
Edge-Based Runtime Verification for the Internet of Things. IEEE Trans. Serv. Comput. 15(5): 2713-2727 (2022) - [c36]Marcello M. Bersani, Chiara Braghin, Angelo Gargantini, Raffaela Mirandola, Elvinia Riccobene, Patrizia Scandurra:
Engineering of Trust Analysis-Driven Digital Twins for a Medical Device. ECSA (Tracks and Workshops) 2022: 467-482 - [c35]Marcello M. Bersani, Chiara Braghin, Vittorio Cortellessa, Angelo Gargantini, Vincenzo Grassi, F. Lo Presti, Raffaela Mirandola, Alfonso Pierantonio, Elvinia Riccobene, Patrizia Scandurra:
Towards Trust-preserving Continuous Co-evolution of Digital Twins. ICSA Companion 2022: 96-99 - [c34]Livia Lestingi, Cristian Sbrolli
Formal Modeling and Verification of Multi-Robot Interactive Scenarios in Service Settings. FormaliSE@ICSE 2022: 80-90 - 2021
- [j13]Livia Lestingi
A Deployment Framework for Formally Verified Human-Robot Interactions. IEEE Access 9: 136616-136635 (2021) - [c33]Robert L. Smith, Marcello M. Bersani, Matteo Rossi, Pierluigi San Pietro:
Improved Bounded Model Checking of Timed Automata. FormaliSE@ICSE 2021: 97-110 - [c32]Mehrnoosh Askarpour
RoboMAX: Robotic Mission Adaptation eXemplars. SEAMS@ICSE 2021: 245-251 - [c31]Christos Tsigkanos, Marcello M. Bersani, Pantelis A. Frangoudis, Schahram Dustdar:
Edge-Based Runtime Verification for the Internet of Things. SERVICES 2021: 16 - [i8]Robert L. Smith, Marcello M. Bersani, Matteo Rossi, Pierluigi San Pietro:
Improved Bounded Model Checking of Timed Automata. CoRR abs/2104.12444 (2021) - 2020
- [j12]Luciano Baresi
Using formal verification to evaluate the execution time of Spark applications. Formal Aspects Comput. 32(1): 33-70 (2020) - [j11]Marcello M. Bersani, Matteo Soldo, Claudio Menghi
PuRSUE -from specification of robotic environments to synthesis of controllers. Formal Aspects Comput. 32(2-3): 187-227 (2020) - [j10]Marcello M. Bersani, Matteo Rossi, Pierluigi San Pietro
On the initialization of clocks in timed formalisms. Theor. Comput. Sci. 813: 175-198 (2020) - [j9]Claudio Menghi
Model Checking MITL Formulae on Timed Automata: A Logic-based Approach. ACM Trans. Comput. Log. 21(3): 26:1-26:44 (2020) - [c30]Mehrnoosh Askarpour
Mind the gap: Robotic Mission Planning Meets Software Engineering. FormaliSE@ICSE 2020: 55-65 - [c29]Livia Lestingi
Formal Verification of Human-Robot Interaction in Healthcare Scenarios. SEFM 2020: 303-324 - [c28]Livia Lestingi
A Model-driven Approach for the Formal Analysis of Human-Robot Interaction Scenarios. SMC 2020: 1907-1914 - [c27]Livia Lestingi
Statistical Model Checking of Human-Robot Interaction Scenarios. AREA@ECAI 2020: 9-17
2010 – 2019
- 2019
- [j8]Marcello M. Bersani, Francesco Marconi, Damian A. Tamburri
Verifying big data topologies by-design : a semi-automated approach. J. Big Data 6: 40 (2019) - [c26]Mehrnoosh Askarpour
Teaching Formal Methods: An Experience Report. FISEE 2019: 3-18 - 2018
- [j7]Marcello M. Bersani
Online verification in cyber-physical systems: Practical bounds for meaningful temporal costs. J. Softw. Evol. Process. 30(3) (2018) - [c25]Damian A. Tamburri
DevOps Service Observability By-Design: Experimenting with Model-View-Controller. ESOCC 2018: 49-64 - [c24]Francesco Marconi
On the Timed Analysis of Big-Data Applications. NFM 2018: 315-332 - [c23]Marcello M. Bersani, Francesco Marconi, Matteo Rossi:
Trace Checking of Streaming Applications through DICE-TraCT. ICPE Companion 2018: 159-160 - [i7]Claudio Menghi, Marcello M. Bersani, Matteo Rossi, Pierluigi San Pietro:
A Flexible Approach for Checking Timed Automata on Continuous Time Semantics. CoRR abs/1806.08684 (2018) - 2017
- [j6]Marcello M. Bersani, Matteo Rossi
A logical characterization of timed regular languages. Theor. Comput. Sci. 658: 46-59 (2017) - [c22]Francesco Marconi, Marcello M. Bersani, Matteo Rossi:
Formal verification of storm topologies through D-VerT. SAC 2017: 1168-1174 - [c21]Marcello M. Bersani, Francesco Marconi, Matteo Rossi, Madalina Erascu
Formal verification of data-intensive applications through model checking modulo theories. SPIN 2017: 98-101 - [c20]Michele Guerriero, Damian A. Tamburri
Towards DevOps for Privacy-by-Design in Data-Intensive Applications: A Research Roadmap. ICPE Companion 2017: 139-144 - 2016
- [j5]Marcello M. Bersani, Matteo Rossi, Pierluigi San Pietro
A tool for deciding the satisfiability of continuous-time metric temporal logic. Acta Informatica 53(2): 171-206 (2016) - [c19]Marcello M. Bersani, Marisol García-Valls
The Cost of Formal Verification in Adaptive CPS. An Example of a Virtualized Server Node. HASE 2016: 39-46 - [c18]Francesco Marconi, Marcello M. Bersani, Madalina Erascu
Towards the Formal Verification of Data-Intensive Applications Through Metric Temporal Logic. ICFEM 2016: 193-209 - [c17]Marcello M. Bersani, Domenico Bianculli
Efficient large-scale trace checking using mapreduce. ICSE 2016: 888-898 - [c16]Marcello M. Bersani, Francesco Marconi, Matteo Rossi, Madalina Erascu
A tool for verification of big-data applications. QUDOS@ISSTA 2016: 44-45 - [c15]Marcello M. Bersani, Francesco Marconi, Damian A. Tamburri
Continuous Architecting of Stream-Based Systems. WICSA 2016: 146-151 - 2015
- [j4]Marcello M. Bersani, Matteo Rossi, Pierluigi San Pietro
An SMT-based approach to satisfiability checking of MITL. Inf. Comput. 245: 72-97 (2015) - [i6]Marcello M. Bersani, Domenico Bianculli, Carlo Ghezzi, Srdan Krstic, Pierluigi San Pietro:
Efficient Large-scale Trace Checking Using MapReduce. CoRR abs/1508.06613 (2015) - 2014
- [j3]Marcello M. Bersani, Achille Frigeri, Angelo Morzenti, Matteo Pradella
Constraint LTL satisfiability checking without automata. J. Appl. Log. 12(4): 522-557 (2014) - [c14]Marcello Maria Bersani, Domenico Bianculli
SMT-Based Checking of SOLOIST over Sparse Traces. FASE 2014: 276-290 - [c13]Marcello M. Bersani, Domenico Bianculli
Towards the formalization of properties of cloud-based elastic systems. PESOS 2014: 38-47 - [c12]Luca Ferrucci
An LTL Semantics of BusinessWorkflows with Recovery. ICSOFT PT 2014: 29-40 - [c11]Marcello M. Bersani, Salvatore Distefano
A Timed Semantics of Workflows. ICSOFT (Selected Papers) 2014: 365-383 - [c10]Marcello M. Bersani, Matteo Rossi, Pierluigi San Pietro
A Logical Characterization of Timed (non-)Regular Languages. MFCS (1) 2014: 75-86 - [e1]Marcello Maria Bersani, Davide Bresolin, Luca Ferrucci
Proceedings First Workshop on Logics and Model-checking for Self-* Systems, MOD* 2014, Bertinoro, Italy, 12th September 2014. EPTCS 168, 2014 [contents] - [i5]Luca Ferrucci, Marcello M. Bersani, Manuel Mazzara:
An LTL Semantics of Business Workflows with Recovery. CoRR abs/1406.1395 (2014) - 2013
- [j2]Marcello Maria Bersani, Matteo Rossi, Pierluigi San Pietro:
On the Satisfiability of Metric Temporal Logics over the Reals. Electron. Commun. Eur. Assoc. Softw. Sci. Technol. 66 (2013) - [j1]Marcello M. Bersani, Achille Frigeri, Alessandra Cherubini:
Expressiveness and complexity of regular pure two-dimensional context-free languages. Int. J. Comput. Math. 90(8): 1708-1733 (2013) - [c9]Marcello M. Bersani, Matteo Rossi, Pierluigi San Pietro
Deciding Continuous-Time Metric Temporal Logic with Counting Modalities. RP 2013: 70-82 - [c8]Marcello M. Bersani, Matteo Rossi, Pierluigi San Pietro
A Tool for Deciding the Satisfiability of Continuous-Time Metric Temporal Logic. TIME 2013: 99-106 - [c7]Marcello Maria Bersani, Matteo Rossi, Pierluigi San Pietro:
Deciding the Satisfiability of MITL Specifications. GandALF 2013: 64-78 - 2012
- [b1]Marcello M. Bersani:
Bounded approaches for verification of infinite-state systems. Polytechnic University of Milan, Italy, 2012 - [i4]Marcello M. Bersani, Achille Frigeri, Angelo Morzenti, Matteo Pradella, Matteo Rossi, Pierluigi San Pietro:
Constraint LTL Satisfiability Checking without Automata. CoRR abs/1205.0946 (2012) - 2011
- [c6]Marcello M. Bersani, Stéphane Demri:
The Complexity of Reversal-Bounded Model-Checking. FroCoS 2011: 71-86 - [c5]Marcello M. Bersani, Achille Frigeri, Alessandra Cherubini:
On Some Classes of 2D Languages and Their Relations. IWCIA 2011: 222-234 - [c4]Marcello M. Bersani, Achille Frigeri, Matteo Rossi, Pierluigi San Pietro
Completeness of the Bounded Satisfiability Problem for Constraint LTL. RP 2011: 58-71 - 2010
- [c3]Marcello M. Bersani, Luca Cavallaro, Achille Frigeri, Matteo Pradella
SMT-based Verification of LTL Specification with Integer Constraints and its Application to Runtime Checking of Service Substitutability. SEFM 2010: 244-254 - [c2]Marcello M. Bersani, Achille Frigeri, Angelo Morzenti, Matteo Pradella
Bounded Reachability for Temporal Logic over Constraint Systems. TIME 2010: 43-50 - [i3]Marcello M. Bersani, Achille Frigeri, Angelo Morzenti, Matteo Pradella, Matteo Rossi, Pierluigi San Pietro:
Bounded Reachability for Temporal Logic over Constraint Systems. CoRR abs/1004.1077 (2010) - [i2]Marcello M. Bersani, Luca Cavallaro, Achille Frigeri, Matteo Pradella, Matteo Rossi:
SMT-based Verification of LTL Specifications with Integer Constraints and its Application to Runtime Checking of Service Substitutability. CoRR abs/1004.2873 (2010)
2000 – 2009
- 2009
- [c1]Marcello M. Bersani, Carlo A. Furia, Matteo Pradella
Integrated Modeling and Verification of Real-Time Systems through Multiple Paradigms. SEFM 2009: 13-22 - [i1]Marcello M. Bersani, Carlo A. Furia, Matteo Pradella, Matteo Rossi:
Integrated Modeling and Verification of Real-Time Systems through Multiple Paradigms. CoRR abs/0907.5074 (2009)
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from ,
, and
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and
to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from .
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-08-05 20:23 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: