It-Matters

Publications

Click here to sort by partners.

2021

Soft constraint automata with memory (WP1) UNIPI
Kasper Dokter, Fabio Gadducci, Benjamin Lion, Francesco Santini.
J. Log. Algebraic Methods Program. , Volume 118, 1-16, 2021.

PomCho: a tool chain for choreographic design (WP3) GSSI
Roberto Guanciale, Emilio Tuosto.
Sci. Comput. Program. , Volume 202, 2021.

2020

Towards a Formal Model for Composable Container Systems (WP1, WP2, WP5) UNIUD
Fabio Burco, Marino Miculan, Marco Peressotti.
Proceedings of the 35th Annual ACM Symposium on Applied Computing (SAC 2020), 2020.

Securing the Art Market with Distributed Public Ledgers (WP5) UNIUD
Marino Miculan, Daniel Tosone.
Editors Franco Chiaraluce, Leonardo Mostarda.
Proceedings of the 3rd Distributed Ledger Technology Workshop (DLT 2020). CEUR Workshop Proceedings, Volume 2580, 2020.

Computing Embeddings of Directed Bigraphs (WP1) UNIUD
Alessio Chiapperini, Marino Miculan, Marco Peressotti.
Editors Fabio Gadducci, Timo Kehrer.
Proceedings of the 13th International Conference on Graph Transformation (ICGT 2020). Lecture Notes in Computer Science, Volume 12150, 38-56, 2020.

Implementation Correctness for Replicated Data Types, Categorically (WP1) UNIPI
Fabio Gadducci, Hernan C. Melgratti, Christian Roldan, Matteo Sammartino.
Editors Violet Ka I Pun, Volker Stolz, Adenilso Simao.
Proceedings of the 17th International Colloquium on Theoretical Aspects of Computing (ICTAC 2020). Lecture Notes in Computer Science, Volume 12545, 283-303, 2020.

An Experience with the Application of Three NLP Tools for the Analysis of Natural Language Requirements (WP3) UNIPI
Monica Arrabito, Alessandro Fantechi, Stefania Gnesi, Laura Semini.
Editors Martin J. Shepperd, Fernando Brito e Abreu, Alberto Rodrigues da Silva, Ricardo Pérez-Castillo.
Proceedings of the 13th International Conference on Quality of Information and Communications Technology (QUATIC 2020). Communications in Computer and Information Science, Volume 1266, 488-498, 2020.

Fluid approximation of broadcasting systems (WP2)
Luca Bortolussi, Jane Hillston, Michele Loreti.
Theor. Comput. Sci. , Volume 816, 221--248, 2020.

Programming interactions in collective adaptive systems by relying on attribute-based communication (WP3)
Yehia Abd Alrahman, Rocco De Nicola, Michele Loreti.
Sci. Comput. Program. , Volume 192, 102428, 2020.

Compositionality of Safe Communication in Systems of Team Automata (WP1, WP2) ISTI
Maurice H. ter Beek, Rolf Hennicker, Jetty Kleijn.
Editors V.K.I. Pun, A. Simao, V. Stolz.
Proceedings of the 17th International Colloquium on Theoretical Aspects of Computing (ICTAC 2020). Lecture Notes in Computer Science, Volume 12545, 200-220, 2020.

30 Years of Simulation-Based Quantitative Analysis Tools: A Comparison Experiment Between Möbius and Uppaal SMC (WP5) ISTI
Davide Basile, Maurice H. ter Beek, Felicita Di Giandomenico, Alessandro Fantechi, Stefania Gnesi, Giorgio O. Spagnolo.
Editors Tiziana Margaria, Bernhard Steffen.
Proceedings of the 9th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles (ISoLA 2020), part I. Lecture Notes in Computer Science, Volume 12476, 368-384, 2020.

Refined Mean Field Analysis: The Gossip Shuffle Protocol Revisited (WP1, WP2) ISTI
Nicolas Gast, Diego Latella, Mieke Massink.
Editors Simon Bliudze, Laura Bocchi.
Proceedings of the 22nd IFIP WG 6.1 International Conference on Coordination Models and Languages (COORDINATION 2020), Held as Part of the 15th International Federated Conference on Distributed Computing Techniques (DisCoTec 2020). Lecture Notes in Computer Science, Volume 12134, 230-239, 2020.

Designing a Demonstrator of Formal Methods for Railways Infrastructure Managers (WP5) ISTI
Davide Basile, Maurice H. ter Beek, Alessandro Fantechi, Alessio Ferrari, Stefania Gnesi, Laura Masullo, Franco Mazzanti, Andrea Piattino, Daniele Trentini.
Editors Tiziana Margaria, Bernhard Steffen.
Proceedings of the 9th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation: Applications (ISoLA 2020), part III. Lecture Notes in Computer Science, Volume 12478, 467-485, 2020.

Family-Based SPL Model Checking Using Parity Games with Variability (WP1, WP2) ISTI
Maurice H. ter Beek, Sjef van Loo, Erik P. de Vink, Tim A. C. Willemse.
Editors Heike Wehrheim, Jordi Cabot.
Proceedings of the 23rd International Conference on Fundamental Approaches to Software Engineering (FASE 2020), Held as Part of the European Joint Conferences on Theory and Practice of Software (ETAPS 2020). Lecture Notes in Computer Science, Volume 12076, 245-265, 2020.
Open Access: ETAPS is open access

Variability meets security: quantitative security modeling and analysis of highly customizable attack scenarios (WP1, WP2) ISTI
Maurice H. ter Beek, Axel Legay, Alberto Lluch-Lafuente, Andrea Vandin.
Editors Maxime Cordy, Mathieu Acher, Danilo Beuche, Gunter Saake.
Proceedings of the 14th International Working Conference on Variability Modelling of Software-Intensive Systems (VaMoS 2020), 11:1-11:9, 2020.

Strategy Synthesis for Autonomous Driving in a Moving Block Railway System with Uppaal Stratego (WP4, WP5) ISTI
Davide Basile, Maurice H. ter Beek, Axel Legay.
Editors Alexey Gotsman, Ana Sokolova.
Proceedings of the 40th IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE 2020), Held as Part of the 15th International Federated Conference on Distributed Computing Techniques (DisCoTec 2020). Lecture Notes in Computer Science, Volume 12136, 3-21, 2020.

Team Automata@Work: On Safe Communication (WP1, WP2) ISTI
Maurice H. ter Beek, Rolf Hennicker, Jetty Kleijn.
Editors Simon Bliudze, Laura Bocchi.
Proceedings of the 22nd IFIP WG 6.1 International Conference on Coordination Models and Languages (COORDINATION 2020), Held as Part of the 15th International Federated Conference on Distributed Computing Techniques (DisCoTec 2020). Lecture Notes in Computer Science, Volume 12134, 77-85, 2020.

Refined Mean Field Analysis: The Gossip Shuffle Protocol Revisited (WP1, WP2) ISTI
Nicolas Gast, Diego Latella, Mieke Massink.
Editors Simon Bliudze, Laura Bocchi.
Proceedings of the 22nd IFIP WG 6.1 International Conference on Coordination Models and Languages (COORDINATION 2020), Held as Part of the 15th International Federated Conference on Distributed Computing Techniques (DisCoTec 2020). Lecture Notes in Computer Science, Volume 12134, 230-239, 2020.

Synthesis of Orchestrations and Choreographies: Bridging the Gap between Supervisory Control and Coordination of Services (WP1, WP4) ISTI
Davide Basile, Maurice H. ter Beek, Rosario Pugliese.
Log. Methods Comput. Sci. , Volume 16, 9:1-9:29, 2020.
Open Access: LMCS is open access

Towards Spatial Bisimilarity for Closure Models: Logical and Coalgebraic Characterisations (WP1) ISTI
Vincenzo Ciancia, Diego Latella, Mieke Massink, Erik P. de Vink.
arXiv:2005.05578 [cs.LO] , 2020.
Open Access: arXiv is open access

Analysing the Provenance of IoT Data (WP1) IMT, UNIPI
Chiara Bodei, Letterio Galletta.
ICISSP (Revised Selected Papers). Communications in Computer and Information Science, Volume 1221, 358-381, 2020.

A True Concurrent Model of Smart Contracts Executions (WP1) IMT
Massimo Bartoletti, Letterio Galletta, Maurizio Murgia.
COORDINATION. Lecture Notes in Computer Science, Volume 12134, 243-260, 2020.

Provably Secure Isolation for Interruptible Enclaved Execution on Small Microprocessors (WP1, WP2) IMT, UNIPI
Matteo Busi, Job Noorman, Jo Van Bulck, Letterio Galletta, Pierpaolo Degano, Jan Tobias Mühlberg, Frank Piessens.
CSF, 262-276, 2020.

Control-flow Flattening Preserves the Constant-Time Policy (WP1, WP2) IMT, UNIPI
Matteo Busi, Pierpaolo Degano, Letterio Galletta.
ITASEC. CEUR Workshop Proceedings, Volume 2597, 82-92, 2020.

MuAC: Access Control Language for Mutual Benefits (WP1) IMT
Lorenzo Ceragioli, Pierpaolo Degano, Letterio Galletta.
ITASEC. CEUR Workshop Proceedings, Volume 2597, 119-127, 2020.

Security Metrics at Work on the Things in IoT Systems (WP1, WP2) IMT, UNIPI
Chiara Bodei, Pierpaolo Degano, Gian Luigi Ferrari, Letterio Galletta.
From Lambda Calculus to Cybersecurity Through Program Analysis. Lecture Notes in Computer Science, Volume 12065, 233-255, 2020.

Verification of Privacy-Enhanced Collaborations (WP1) IMT, UNICAM
Sara Belluccini, Rocco De Nicola, Marlon Dumas, Pille Pullonen, Barbara Re, Francesco Tiezzi.
FormaliSE@ICSE, 141-152, 2020.

Natural Projection as Partial Model Checking (WP1) IMT, UNIPI
Costa, Gabriele, Galletta, Letterio, Degano, Pierpaolo, Basin, David, Bodei, Chiara.
Journal of Automated Reasoning , 1-37, 2020.

The DReAM framework for dynamic reconfigurable architecture modelling: theory and applications (WP3) IMT
Rocco De Nicola, Alessandro Maggi, Joseph Sifakis.
Int. J. Softw. Tools Technol. Transf. , Volume 22, 437-455, 2020.

Rigorous engineering of collective adaptive systems: special section (WP1, WP2) IMT
Rocco De Nicola, Stefan Jähnichen, Martin Wirsing.
Int. J. Softw. Tools Technol. Transf. , Volume 22, 389-397, 2020.

Natural Projection as Partial Model Checking (WP1) IMT, UNIPI
Costa, Gabriele, Galletta, Letterio, Degano, Pierpaolo, Basin, David, Bodei, Chiara.
Journal of Automated Reasoning , 1--37, 2020.

The DReAM framework for dynamic reconfigurable architecture modelling: theory and applications (WP3) IMT
Rocco De Nicola, Alessandro Maggi, Joseph Sifakis.
Int. J. Softw. Tools Technol. Transf. , Volume 22, 437--455, 2020.

A formal approach to the engineering of domain-specific distributed systems (WP1) IMT, UNICAM
Rocco De Nicola, Gian Luigi Ferrari, Rosario Pugliese, Francesco Tiezzi.
J. Log. Algebraic Methods Program. , Volume 111, 100511, 2020.

A Choreography-Driven Approach to APIs: The OpenDXL Case Study (WP3, WP4) GSSI
Leonardo Frittelli, Facundo Maldonado, Hernán C. Melgratti, Emilio Tuosto.
Editors Simon Bliudze, Laura Bocchi.
Proceedings of the 22nd IFIP WG 6.1 International Conference on Coordination Models and Languages (COORDINATION 2020), Held as Part of the 15th International Federated Conference on Distributed Computing Techniques (DisCoTec 2020). Lecture Notes in Computer Science, Volume 12134, 107-124, 2020.

Choreography Automata (WP3) GSSI
Franco Barbanera, Ivan Lanese, Emilio Tuosto.
Editors Simon Bliudze, Laura Bocchi.
Proceedings of the 22nd IFIP WG 6.1 International Conference on Coordination Models and Languages (COORDINATION 2020), Held as Part of the 15th International Federated Conference on Distributed Computing Techniques (DisCoTec 2020). Lecture Notes in Computer Science, Volume 12134, 86-106, 2020.
Open Access: available here

Choreographic Development of Message-Passing Applications - A Tutorial (WP3, WP4) GSSI
Alex Coto, Roberto Guanciale, Emilio Tuosto.
Editors Simon Bliudze, Laura Bocchi.
Proceedings of the 22nd IFIP WG 6.1 International Conference on Coordination Models and Languages (COORDINATION 2020), Held as Part of the 15th International Federated Conference on Distributed Computing Techniques (DisCoTec 2020). Lecture Notes in Computer Science, Volume 12134, 20-36, 2020.

Composing Communicating Systems, Synchronously (WP2) GSSI
Franco Barbanera, Ivan Lanese, Emilio Tuosto.
Proceedings of ISoLA 2020. Lecture Notes in Computer Science, Volume 12476, 39-59, 2020.

Abstractions for Collective Adaptive Systems (WP3) GSSI
Omar Inverso, Catia Trubiani, Emilio Tuosto.
Proceedings of ISoLA 2020. Lecture Notes in Computer Science, Volume 12477, 243-260, 2020.

Tight Error Analysis in Fixed-point Arithmetics (WP3) GSSI, IMT
Stella Simic, Alberto Bemporad, Omar Inverso, Mirco Tribastone.
Editors Rajiv Gupta, Xipeng Shen.
Proceedings of iFM. Lecture Notes in Computer Science, Volume 12546, 318-336, 2020.

Parallel and distributed bounded model checking of multi-threaded programs (WP3) GSSI
Omar Inverso, Catia Trubiani.
Editors Rajiv Gupta, Xipeng Shen.
PPoPP'20: 25th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, 202-216, 2020.

Probabilistic Analysis of Binary Sessions (WP2) GSSI
Omar Inverso, Hernán C. Melgratti, Luca Padovani, Catia Trubiani, Emilio Tuosto.
Editors Igor Konnov, Laura Kovács.
Proceedings of the 31st International Conference on Concurrency Theory (CONCUR 2020). LIPIcs, Volume 171, 14:1-14:21, 2020.
Open Access: LIPIcs publications are open access

Verifying AbC specifications via emulation (WP3) GSSI, IMT
Rocco De Nicola, Tan Duon, Omar Inverso.
Proceedings of ISoLA 2020. Lecture Notes in Computer Science, Volume 12477, 261-279, 2020.

On Testing Message-Passing Components (WP3) GSSI
Alex Coto, Roberto Guanciale, Emilio Tuosto.
Proceedings of ISoLA 2020. Lecture Notes in Computer Science, Volume 12476, 22-38, 2020.

Combining SLiVER with CADP to Analyze Multi-agent Systems (WP3) GSSI
Luca Di Stefano, Frédéric Lang, Wendelin Serwe.
Editors Simon Bliudze, Laura Bocchi.
Proceedings of the 22nd IFIP WG 6.1 International Conference on Coordination Models and Languages (COORDINATION 2020), Held as Part of the 15th International Federated Conference on Distributed Computing Techniques (DisCoTec 2020). Lecture Notes in Computer Science, Volume 12134, 370-385, 2020.

An Abstract Framework for Choreographic Testing (WP3, WP4) GSSI
Alex Coto, Roberto Guanciale, Emilio Tuosto.
ICE 2020, Volume abs/2009.07991, 2020.
Open Access: EPTCS is open access

Towards Refinable Choreographies (WP2) GSSI
Ugo de'Liguoro, Hernán C. Melgratti, Emilio Tuosto.
ICE, Volume abs/2009.07991, 2020.
Open Access: EPTCS is open access

Automated Model-based Performance Analysis of Software Product Lines under Uncertainty (WP4) GSSI
Paolo Arcaini, Omar Inverso, Catia Trubiani.
Information and Software Technology , Volume 127, 2020.

Multi-agent systems with virtual stigmergy (WP3) GSSI, IMT
Rocco De Nicola, Luca Di Stefano, Omar Inverso.
Sci. Comput. Program. , Volume 187, 102345, 2020.

The complexity of identifying characteristic formulae (WP4) GSSI
Luca Aceto, Antonis Achilleos, Adrian Francalanza, Anna Ingólfsdóttir.
J. Log. Algebraic Methods Program. , Volume 112, 100529, 2020.
Open Access: available here

Determinizing monitors for HML with recursion (WP4) GSSI
Luca Aceto, Antonis Achilleos, Adrian Francalanza, Anna Ingólfsdóttir, Sævar Örn Kjartansson.
Journal of Logical and Algebraic Methods in Programming , Volume 111, 100515, 2020.
Open Access: available here

2019

An Abstract Distributed Middleware for Transactions over Heterogeneous Stores (WP3) UNIUD
Luca Geatti, Federico Igne, Marino Miculan.
Editors Alessandra Cherubini, Nicoletta Sabadini, Simone Tini.
Proceedings of the 20th Italian Conference on Theoretical Computer Science (ICTCS 2019). CEUR Workshop Proceedings, Volume 2504, 171-183, 2019.

LF+ in Coq for ``fast and loose'' reasoning (WP3) UNIUD
Fabio Alessi, Alberto Ciaffaglione, Pietro Di Gianantonio, Furio Honsell, Marina Lenisa, Ivan Scagnetto.
J. Formaliz. Reason. , Volume 12, 11-51, 2019.

A Categorical Account of Replicated Data Types (WP1) UNIPI
Fabio Gadducci, Hernan C. Melgratti, Christian Roldan, Matteo Sammartino.
Editors Arkadev Chattopadhyay, Paul Gastin.
Proceedings of the 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019). LIPIcs, Volume 150, 42:1-42:15, 2019.

Data-Driven Choreographies a la Klaim (WP1, WP4) UNIPI, GSSI
Roberto Bruni, Andrea Corradini, Fabio Gadducci, Hernán C. Melgratti, Ugo Montanari, Emilio Tuosto.
Editors Michele Boreale, Flavio Corradini, Michele Loreti, Rosario Pugliese.
Models, Languages, and Tools for Concurrent and Distributed Programming. Lecture Notes in Computer Science, Volume 11665, 170-190, 2019.

Polyadic Soft Constraints (WP1) UNIPI
Filippo Bonchi, Laura Bussi, Fabio Gadducci, Francesco Santini.
Editors Mário S. Alvim, Kostas Chatzikokolakis, Carlos Olarte, Frank Valencia.
The Art of Modelling Computational Systems: A Journey from Logic and Concurrency to Security and Privacy. Lecture Notes in Computer Science, Volume 11760, 241-257, 2019.

Petri nets are dioids: a new algebraic foundation for non-deterministic net theory (WP1) UNIPI
Paolo Baldan, Fabio Gadducci.
Acta Informatica , Volume 56, 61-92, 2019.

Innovating Medical Image Analysis via Spatial Logics (WP1) ISTI
Gina Belmonte, Vincenzo Ciancia, Diego Latella, Mieke Massink.
Editors Maurice H. ter Beek, Alessandro Fantechi, Laura Semini.
From Software Engineering to Formal Methods and Tools, and Back. Lecture Notes in Computer Science, Volume 11865, 85-109, 2019.

Embedding RCC8D in the Collective Spatial Logic CSLCS (WP1) ISTI
Vincenzo Ciancia, Diego Latella, Mieke Massink.
Editors Michele Boreale, Flavio Corradini, Michele Loreti, Rosario Pugliese.
Models, Languages, and Tools for Concurrent and Distributed Programming. Lecture Notes in Computer Science, Volume 11665, 260-277, 2019.

Comparing Controlled System Synthesis and Suppression Enforcement (WP4) GSSI
Luca Aceto, Ian Cassar, Adrian Francalanza, Anna Ingólfsdóttir.
Editors Bernd Finkbeiner, Leonardo Mariani.
Proceedings of the 19th International Conference on Runtime Verification (RV 2019). Lecture Notes in Computer Science, Volume 11757, 148-164, 2019.

An Operational Guide to Monitorability (WP4) GSSI
Luca Aceto, Antonis Achilleos, Adrian Francalanza, Anna Ingólfsdóttir, Karoliina Lehtinen.
Editors Peter Csaba Ölveczky, Gwen Salaün.
Proceedings of the 17th International Conference on Software Engineering and Formal Methods (SEFM 2019). Lecture Notes in Computer Science, Volume 11724, 433-453, 2019.

Unpublished Manuscripts

On Monitoring Asynchronous Components, Asynchronously
Luca Aceto, Duncan Paul Attard, Adrian Francalanza, Anna Ingólfsdóttir.
Submitted for conference publication (WP4) GSSI

On Benchmarking for Concurrent Runtime Monitoring
Luca Aceto, Duncan Paul Attard, Adrian Francalanza, Anna Ingólfsdóttir.
Submitted for conference publication (WP4) GSSI

The best a monitor can do
Luca Aceto, Antonis Achilleos, Adrian Francalanza, Anna Ingólfsdóttir, Karoliina Lehtinen.
Submitted for conference publication (WP4) GSSI

An Operational Guide to Monitorability
Luca Aceto, Antonis Achilleos, Adrian Francalanza, Anna Ingólfsdóttir, Karoliina Lehtinen.
Submitted to the journal Software and Systems Modeling, Springer (WP4) GSSI

Semantics-based Verification of Concurrent Systems via Sequential Reachability or Termination
Luca Di Stefano, Omar Inverso, Rocco De Nicola.
Submitted for conference publication (WP3, WP4) GSSI, IMT

Unavailable Transit Feed Specification: Making it Available with Recurrent Neural Networks
Ludovico Iovino, Phuong T. Nguyen, Amleto Di Salle, Francesco Gallo, Michele Flammini.
Submitted to conference

Composition and Decomposition of Multiparty Sessions
Franco Barbanera, Mariangiola Dezani-Ciancaglini, Ivan Lanese, Emilio Tuosto.
Submitted to JLAMP (WP3) GSSI