Publications

Journal papers:


2020
C. Menghi, M.M. Bersani, M. Rossi, P. San Pietro
Model Checking MITL formulae on Timed Automata: a Logic-Based Approach     --    (NEW!)
Transaction of Computational Logic (accepted, typesetting)

M.M. Bersani, C. Menghi, P. Pelliccione, M. Rossi, M. Soldo
PuRSUE - From Specification of Robotic Environments to Synthesis of Controllers     --    (NEW!)
Formal Aspects of Computing (accepted provided minor typographic revision)

L. Baresi, M.M. Bersani, F. Marconi, G. Quattrocchi and M. Rossi
Using Formal Verification to Evaluate the Execution Time of Spark Applications Formal Aspects of Computing
    --    (NEW!)
Formal Aspects of Computing
DOI: 10.1007/s00165-020-00505-4

2019
M.M. Bersani, M. Rossi, P. San Pietro
On the Initialization of Clocks in Timed Formalisms     --    (NEW!)
Theoretical Computer Science
DOI: 10.1016/j.tcs.2019.11.023

M.M. Bersani, F. Marconi, D.A. Tamburri, A. Nodari, P. Jamshidi
Verifying Big Data Topologies By-Design: a Semi-Automated Approach
Journal of Big Data 6:40
DOI: 10.1186/s40537-019-0199-y

2018
M.M.Bersani, M. Garcia-Valls
Online verification in cyber-physical systems: Practical bounds for meaningful temporal costs
Journal of Software: Evolutions and Process
DOI: 10.1002/smr.1880

2017
M.M. Bersani, M. Rossi, P. San Pietro
A Logical Characterization of Timed Regular Languages
Theoretical Computer Science 658:46-59
DOI: 10.1016/j.tcs.2016.07.020

2016
M.M. Bersani, M. Rossi, P. San Pietro
A Tool for Deciding the Satisfiability of Continuous-time Metric Temporal Logic
Acta Informatica 53(2): 171-206
DOI: 10.1007/s00236-015-0229-y


2015
M.M. Bersani, M. Rossi, P. San Pietro
An SMT-based Approach to Satisfiability Checking of MITL
Information and Computation 245: 72-97
DOI: 10.1016/j.ic.2015.06.007


2014
M.M. Bersani, A. Frigeri, A. Morzenti, M. Pradella, M. Rossi, P. San Pietro
Constraint LTL Satisfiability Checking without Automata
Journal of Applied Logics 12(4): 522-557
DOI: 10.1016/j.jal.2014.07.005

2013
M.M. Bersani, A. Frigeri, A. Cherubini
Expressiveness and Complexity of Regular Pure two-dimensional Context-free Languages
International Journal of Computer Mathematics 90(8): 1708-1733
DOI: 10.1080/00207160.2013.787143




Conference papers:

2018
D.A. Tamburri, M.M. Bersani, R. Mirandola, G. Pea
DevOps Service Observability By-Design: Experimenting with Model-View-Controller
European Conference on Service-oriented and Cloud Computing-ESOCC 2018:49-64
DOI: 10.1007/978-3-319-99819-0_4

F. Marconi, G. Quattrocchi, L. Baresi, M.M. Bersani, M. Rossi
On the Timed Analysis of Big-Data Applications
Nasa Formal Methods - NFM 2018:315-332
DOI: 10.1007/978-3-319-77935-5_22

2017
F. Marconi, M.M. Bersani, M. Rossi
Formal Verification of Storm Topologies through D-verT
Software Architecture: Theory, Technology, and Applications - SATTA, SAC 2017:1168-1174
DOI: 10.1145/3019612.3019769

M.M. Bersani, F. Marconi, M. Rossi,M. Erascu, S. Ghilardi
Formal verification of data-intensive applications through model checking modulo theories
SPIN 2017:98-101
DOI: 10.1145/3092282.3092300

2016
F. Marconi, M.M. Bersani, M. Erascu, M. Rossi
Towards the formal verification of data-intensive applications through metric temporal logic
International Conference on Formal Engineering Methods, ICFEM 2016:193-209
DOI: 10.1007/978-3-319-47846-3_13

M.M. Bersani, F. Marconi, D. A. Tamburri, P. Jamshidi, A. Nodari
Continuous Architecting of Stream-Based Systems
Working IEEE/IFIP Conference on Software Architecture - WICSA 2016:146-151
DOI: 10.1109/WICSA.2016.26

M.M. Bersani, D. Bianculli, C. Ghezzi, S. Krstic, P. San Pietro
Efficient Large-scale Trace Checking Using MapReduce
International Conference of Software Engeneering - ICSE 2016:888-898
DOI: 10.1145/2884781.2884832

M.M. Bersani, M. García-Valls
The Cost of Formal Verification in adaptive CPS. An example of a virtualized node
High Assurance Software Engineering - HASE 2016:39-46
DOI: 10.1109/HASE.2016.46

2014
M.M. Bersani, D. Bianculli, C. Ghezzi, S. Krstic, P. San Pietro
SMT-Based Checking of SOLOIST over Sparse Traces
Fundamental Approaches to Software Engineering - FASE 2014:276-290
DOI: 10.1007/978-3-642-54804-8_19

L. Ferrucci, M. M. Bersani, M. Mazzara
An LTL Semantics of Business Workflows with Recovery
International Conference on Software Paradigm Trends - ICSOFT PT 2014:29-40
DOI: 10.5220/0005110000290040

M. M. Bersani, S. Distefano, L. Ferrucci, M. Mazzara
A Timed Semantics of Workflows
Selected Paper of International Conference on Software Paradigm Trends - ICSOFT
PT 2014:365-383
DOI: 10.1007/978-3-319-25579-8_21

M.M. Bersani, M. Rossi, P. San Pietro
A Logical Characterization of Timed (non-)Regular Languages
Mathematical Foundation of Computer Science - MFCS 2014:75-86
DOI: 10.1007/978-3-662-44522-8_7

2013
M.M. Bersani, M. Rossi, P. San Pietro
Deciding Continuous-Time Metric Temporal Logic with Counting Modalities
Reachability Problems - RP 2013:70-82
DOI: 10.1007/978-3-642-41036-9_8

M.M. Bersani, M. Rossi, P. San Pietro
Deciding the Satisfiability of MITL Specifications
Games and Automata, Languages, Formal Verification - GandALF 2013:64-78
DOI: 10.4204/EPTCS.119.8

M.M. Bersani, M. Rossi, P. San Pietro
A Tool for Deciding the Satisfiability of Continuous-time Metric Temporal Logic
Symposium on Temporal Representation and Reasoning - TIME 2013:99-106
DOI: 10.1109/TIME.2013.20

2011
M.M. Bersani, S. Demri
The Complexity of Reversal-Bounded Model-Checking
Frontiers of Combining systems - FroCoS 2011:71-86
DOI: 10.1007/978-3-642-24364-6_6

M.M. Bersani, A. Frigeri, M. Rossi, P. San Pietro
Completeness of the Bounded Satisfiability Problem for Constraint LTL
Reachability Problems - RP 2011:58-71
DOI: 10.1007/978-3-642-24288-5_7

2010
M.M. Bersani, A. Frigeri, A. Morzenti, M. Pradella, M. Rossi, P. San Pietro
Bounded Reachability for Temporal Logic over Constraint Systems
Symposium on Temporal Representation and Reasoning - TIME 2010:43-50
DOI: 10.1109/TIME.2010.21

M.M. Bersani, L. Cavallaro, A. Frigeri, M. Pradella, M. Rossi
SMT-based Verification of LTL Specifications with Integer Constraints and its Application to Runtime Checking of Service Substitutability
Software Engineering and Formal Methods - SEFM 2010:244-254
DOI: 10.1109/SEFM.2010.37

2009
M.M. Bersani, C.A. Furia, M. Pradella, M. Rossi
Integrated Modeling and Verification of Real-Time Systems through Multiple Paradigms
Software Engineering and Formal Methods - SEFM 2009:13-22
10.1109/SEFM.2009.16



Workshop papers:

2018
M. M. Bersani, F. Marconi, M. Rossi
Trace Checking of Streaming Applications through DICE-TraCT
International Conference on Performance Engineering - ICPE 2018:159-160
DOI: 10.1145/3185768.3186287

2017
M. Guerriero, D.A. Tamburri, Y. Ridene, F. Marconi, M.M. Bersani, M. Artac
Towards DevOps for Privacy-by-Design in Data-Intensive Applications: a Research Roadmap
International Conference on Performance Engineering - ICPE 2017: 139-144
DOI: 10.1145/3053600.3053631

2016
M.M. Bersani, F. Marconi, M. Rossi, M. Erascu
A tool for Verification of Big-data Applications
2nd International Workshop on Quality-Aware DevOps, QUDOS 2016:44-45
DOI: 10.1145/2945408.2945419

2014
M. M. Bersani, D. Bianculli, S. Dustdar, A. Gambi, C. Ghezzi, S. Krstic
Towards the formalization of properties of cloud-based elastic systems
Principles of Engineering Service-Oriented and Cloud Systems - PESOS 2014:38-47
DOI: 10.1145/2593793.2593798

2013
M.M. Bersani, M. Rossi, P. San Pietro
On the Satisfiability of Metric Temporal Logics over the Reals
Workshop on Automated Verification of Critical Systems - AVOCS 2013

M.M. Bersani, A. Cherubini, A. Frigeri
On some Classes of 2D Languages and their Relations
Workshop on Combinatorial Image Analysis - IWCIA 2011:222-234
DOI: 10.1007/978-3-642-21073-0_21