It-Matters

Publications

Click here to sort by partners.

2023

Research Challenges in Orchestration Synthesis (WP2, WP3) ISTI
Davide Basile, Maurice H. ter Beek.
Editors Clément Aubert, Cinzia Di Giusto, Simon Fowler, Larisa Safina.
Proceedings of the 16th Interaction and Concurrency Experience (ICE'23). Electronic Proceedings in Theoretical Computer Science, Volume , , 2023.

A Runtime Environment for Contract Automata (WP2, WP3, WP4) ISTI
Davide Basile, Maurice H. ter Beek.
Editors Marsha Chechik, Joost-Pieter Katoen, Martin Leucker.
Proceedings of the 25th International Symposium on Formal Methods (FM'23). Lecture Notes in Computer Science, Volume 14000, 550--567, 2023.

Can We Communicate? Using Dynamic Logic to Verify Team Automata (WP1, WP2) ISTI
Maurice H. ter Beek, Guillermina Cledou, Rolf Hennicker, José Proença.
Editors Marsha Chechik, Joost-Pieter Katoen, Martin Leucker.
Proceedings of the 25th International Symposium on Formal Methods (FM'23). Lecture Notes in Computer Science, Volume 14000, 122--141, 2023.

On Bisimilarity for Polyhedral Models and {SLCS} (WP1, WP2, WP5) ISTI
Vincenzo Ciancia, David Gabelaia, Diego Latella, Mieke Massink, Erik P. de Vink.
Editors Marieke Huisman, António Ravara.
Formal Techniques for Distributed Objects, Components, and Systems - 43rd {IFIP} {WG} 6.1 International Conference, {FORTE} 2023, Held as Part of the 18th International Federated Conference on Distributed Computing Techniques, DisCoTec 2023, Lisbon, Portugal, June 19-23, 2023, Proceedings. Lecture Notes in Computer Science, Volume 13910, 132--151, 2023.

Minimisation of Spatial Models Using Branching Bisimilarity (WP1, WP2, WP5) ISTI
Vincenzo Ciancia, Jan Friso Groote, Diego Latella, Mieke Massink, Erik P. de Vink.
Editors Marsha Chechik, Joost-Pieter Katoen, Martin Leucker.
Formal Methods - 25th International Symposium, {FM} 2023, L{"{u}}beck, Germany, March 6-10, 2023, Proceedings. Lecture Notes in Computer Science, Volume 14000, 263--281, 2023.

A Toolchain for Strategy Synthesis with Spatial Properties (WP2, WP5) ISTI
Davide Basile, Maurice H. ter Beek, Laura Bussi, Vincenzo Ciancia.
Int. J. Softw. Tools Technol. Transf. , Volume , , 2023.

2022

An Experimental Toolchain for Strategy Synthesis with Spatial Properties (WP2, WP5) ISTI
Davide Basile, Maurice H. ter Beek, Vincenzo Ciancia.
Editors Tiziana Margaria, Bernhard Steffen.
Proceedings of the 11th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation: Adaptation and Learning (ISoLA'22). Lecture Notes in Computer Science, Volume 13703, 142--164, 2022.

On Binding in the Spatial Logics for Closure Spaces (WP1, WP2, WP5) ISTI
Laura Bussi, Vincenzo Ciancia, Fabio Gadducci, Diego Latella, Mieke Massink.
Editors Tiziana Margaria, Bernhard Steffen.
Leveraging Applications of Formal Methods, Verification and Validation. Verification Principles - 11th International Symposium, ISoLA 2022, Rhodes, Greece, October 22-30, 2022, Proceedings, Part {I}. Lecture Notes in Computer Science, Volume 13701, 479--497, 2022.

Back-and-Forth in Space: On Logics and Bisimilarity in Closure Spaces (WP1, WP2, WP5) ISTI
Vincenzo Ciancia, Diego Latella, Mieke Massink, Erik P. de Vink.
Editors Nils Jansen, Mariëlle Stoelinga, Petra van den Bos.
A Journey from Process Algebra via Timed Automata to Model Learning - Essays Dedicated to Frits Vaandrager on the Occasion of His 60th Birthday. Lecture Notes in Computer Science, Volume 13560, 98--115, 2022.

Towards a GUI for Declarative Medical Image Analysis: Cognitive and Memory Load Issues (WP5) ISTI
Giovanna Broccia, Vincenzo Ciancia, Diego Latella, Mieke Massink.
Editors Constantine Stephanidis, Margherita Antona, Stavroula Ntoa.
{HCI} International 2022 Posters - 24th International Conference on Human-Computer Interaction, {HCII} 2022, Virtual Event, June 26 - July 1, 2022, Proceedings, Part {II}. Communications in Computer and Information Science, Volume 1581, 103--111, 2022.

Contract Automata Library (WP2, WP3) ISTI
Davide Basile, Maurice H. ter Beek.
Sci. Comput. Program. , 2022.

Exploring the ERTMS/ETCS full moving block specification: an experience with formal methods (WP2, WP5) ISTI
Davide Basile, Maurice H. ter Beek, Alessio Ferrari, Axel Legay.
Int. J. Softw. Tools Technol. Transf. , Volume 24, 351--370, 2022.

Geometric Model Checking of Continuous Space (WP1, WP2, WP5) ISTI
Nick Bezhanishvili, Vincenzo Ciancia, David Gabelaia, Gianluca Grilletti, Diego Latella, Mieke Massink.
Log. Methods Comput. Sci. , Volume 18, 2022.

2021

Composable Partial Multiparty Session Types (WP3, WP4) UNIUD
Claude Stolze, Marino Miculan, Di Gianantonio, Pietro.
Proc.~17th International Conference on Formal Aspects of Component Software (FACS) [to appear]. LNCS, 2021.

Closure hyperdoctrines (WP1) UNIUD
Davide Castelnovo, Marino Miculan.
9th Conference on Algebra and Coalgebra in Computer Science [to appear]. LIPIcs, 2021.

A Calculus for Attribute-Based Memory Updates (WP3) UNIUD
Marino Miculan, Michele Pasqua.
Editors Antonio Cerone, Peter Csaba Ölveczky.
Theoretical Aspects of Computing - {ICTAC} 2021 - 18th International Colloquium, Virtual Event, Nur-Sultan, Kazakhstan, September 8-10, 2021, Proceedings. Lecture Notes in Computer Science, Volume 12819, 366--385, 2021.

A time-series classification approach to shallow web traffic de-anonymization (WP3) UNIUD
De Nardin, Axel, Marino Miculan, Claudio Piciarelli, Foresti, Gian Luca.
Editors Alessandro Armando, Michele Colajanni.
5th italian conference on cyber security (ITASEC). CEUR-WS, Volume 2940, 7:1--7:18, 2021.

A protoype-based approach to object evolution (WP3) UNIUD
Alberto Ciaffaglione, Pietro Di Gianantonio, Furio Honsell, Luigi Liquori.
J. Object Technol. , Volume 20, 2021.

Nets with Mana: A Framework for Chemical Reaction Modelling (WP1) UNIPI
Fabrizio Romano Genovese, Fosco Loregian, Daniele Palombi.
Graph Transformation - 14th International Conference, {ICGT} 2021, Held as Part of {STAF} 2021, Virtual Event, June 24-25, 2021, Proceedings. LNCS, 2021.

A categorical semantics for hierarchical Petri Nets (WP1) UNIPI
Fabrizio Romano Genovese, Jelle Harold, Fosco Loregian, Daniele Palombi.
12th International Workshop on Graph Computation Models, GCM : Held as Part of STAF 2021, Virtual Event, June 22 2021. Proceedings [to appear]. EPTCS, 2021.

The Gödel Fibration (WP1) UNIPI
Davide Trotta, Matteo Spadetto, Valeria de Paiva.
Editors Filippo Bonchi, Simon J. Puglisi.
46th International Symposium on Mathematical Foundations of Computer Science, {MFCS} 2021, August 23-27, 2021, Tallinn, Estonia. LIPIcs, Volume 202, 87:1--87:16, 2021.
Open Access: Available here

A Tool for {JSON} Schema Witness Generation (WP1, WP2) UNIPI
Lyes Attouche, Mohamed Amine Baazizi, Dario Colazzo, Francesco Falleni, Giorgio Ghelli, Cristiano Landi, Carlo Sartiani, Stefanie Scherzinger.
Editors Yannis Velegrakis, Demetris Zeinalipour-Yazti, Panos K. Chrysanthis, Francesco Guerra.
Proceedings of the 24th International Conference on Extending Database Technology, {EDBT} 2021, Nicosia, Cyprus, March 23 - 26, 2021, 694--697, 2021.
Open Access: Available here

Residuation for Soft Constraints: Lexicographic Orders and Approximation Techniques (WP1) UNIPI
Fabio Gadducci, Francesco Santini.
Editors Wolfgang Faber, Gerhard Friedrich, Martin Gebser, Michael Morak.
Logics in Artificial Intelligence - 17th European Conference, {JELIA} 2021, Virtual Event, May 17-20, 2021, Proceedings. Lecture Notes in Computer Science, Volume 12678, 162--176, 2021.

Language and Communication Problems in Formalization: {A} Natural Language Approach (WP1) UNIPI
Alessandro Fantechi, Stefania Gnesi, Laura Semini.
Editors Alexander Raschke, Elvinia Riccobene, Klaus-Dieter Schewe.
Logic, Computation and Rigorous Methods - Essays Dedicated to Egon B{"{o}}rger on the Occasion of His 75th Birthday. Lecture Notes in Computer Science, Volume 12750, 121--134, 2021.

Towards a Spatial Model Checker on GPU (WP1, WP2) UNIPI, ISTI
Laura Bussi, Vincenzo Ciancia, Fabio Gadducci.
Editors Kirstin Peters, Tim A. C. Willemse.
Proceedings of the 41st IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE'21). Lecture Notes in Computer Science, Volume 12719, 188--196, 2021.

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

How Adaptive and Reliable is Your Program? (WP2) UNICAM
Valentina Castiglioni, Michele Loreti, Simone Tini.
Editors Kirstin Peters, Tim A. C. Willemse.
Formal Techniques for Distributed Objects, Components, and Systems - 41st {IFIP} {WG} 6.1 International Conference, {FORTE} 2021, Held as Part of the 16th International Federated Conference on Distributed Computing Techniques, DisCoTec 2021, Valletta, Malta, June 14-18, 2021, Proceedings. Lecture Notes in Computer Science, Volume 12719, 60--79, 2021.

Provably correct implementation of the AbC calculus (WP3) UNICAM, IMT
Rocco De Nicola, Tan Duong, Michele Loreti.
Sci. Comput. Program. , Volume 202, 102567, 2021.

Spatial Model Checking for Smart Stations: Research Challenges (WP2, WP5) ISTI
Maurice H. ter Beek, Vincenzo Ciancia, Diego Latella, Mieke Massink, Giorgio Oronzo Spagnolo.
Editors Alberto Lluch-Lafuente, Anastasia Mavridou.
Proceedings of the 26th International Conference Formal Methods for Industrial Critical Systems (FMICS'21). Lecture Notes in Computer Science, Volume 12863, 39--47, 2021.

Featured Team Automata (WP1, WP2) ISTI
Maurice H. ter Beek, Guillermina Cledou, Rolf Hennicker, Jose Proenca.
Editors Marieke Huisman, Corina S. Pasareanu, Naijun Zhan.
Proceedings of the 24th International Symposium on Formal Methods (FM'21). Lecture Notes in Computer Science, Volume 13047, 483--502, 2021.

A Clean and Efficient Implementation of Choreography Synthesis for Behavioural Contracts (WP1, WP2) ISTI
Davide Basile, Maurice H. ter Beek.
Editors Ferruccio Damiani, Ornela Dardha.
Proceedings of the 23rd IFIP WG 6.1 International Conference on Coordination Models and Languages (COORDINATION'21). Lecture Notes in Computer Science, Volume 12717, 225--238, 2021.

A Hands-On Introduction to Spatial Model Checking Using VoxLogicA - - Invited Contribution (WP5) ISTI
Vincenzo Ciancia, Gina Belmonte, Diego Latella, Mieke Massink.
Editors Alfons Laarman, Ana Sokolova.
Model Checking Software - 27th International Symposium, {SPIN} 2021, Virtual Event, July 12, 2021, Proceedings. Lecture Notes in Computer Science, Volume 12864, 22--41, 2021.

Querying Medical Imaging Datasets Using Spatial Logics (Position Paper) (WP5) ISTI
Gina Belmonte, Giovanna Broccia, Laura Bussi, Vincenzo Ciancia, Diego Latella, Mieke Massink.
Editors Ladjel Bellatreche, George A. Chernishev, Antonio Corral, Samir Ouchani, Jüri Vain.
Advances in Model and Data Engineering in the Digitalization Era - {MEDI} 2021 International Workshops: DETECT, SIAS, CSMML, BIOC, HEDA, Tallinn, Estonia, June 21-23, 2021, Proceedings. Communications in Computer and Information Science, Volume 1481, 285--301, 2021.

Feasibility of Spatial Model Checking for Nevus Segmentation (WP5) ISTI
Gina Belmonte, Giovanna Broccia, Vincenzo Ciancia, Diego Latella, Mieke Massink.
Editors Simon Bliudze, Stefania Gnesi, Nico Plat, Laura Semini.
9th {IEEE/ACM} International Conference on Formal Methods in Software Engineering, FormaliSE@ICSE 2021, Madrid, Spain, May 17-21, 2021, 1--12, 2021.

Towards a Spatial Model Checker on GPU (WP1, WP2, WP5) ISTI
Laura Bussi, Vincenzo Ciancia, Fabio Gadducci.
Editors Kirstin Peters, Tim A. C. Willemse.
Formal Techniques for Distributed Objects, Components, and Systems - 41st {IFIP} {WG} 6.1 International Conference, {FORTE} 2021, Held as Part of the 16th International Federated Conference on Distributed Computing Techniques, DisCoTec 2021, Valletta, Malta, June 14-18, 2021, Proceedings. Lecture Notes in Computer Science, Volume 12719, 188--196, 2021.

Towards Model Checking Video Streams Using VoxLogicA on GPUs (WP1, WP2, WP5) ISTI
Laura Bussi, Vincenzo Ciancia, Fabio Gadducci, Diego Latella, Mieke Massink.
Editors Juliana Bowles, Giovanna Broccia, Roberto Pellungrini.
From Data to Models and Back - 10th International Symposium, DataMod 2021, Virtual Event, December 6-7, 2021, Revised Selected Papers. Lecture Notes in Computer Science, Volume 13268, 78--90, 2021.

FWS: Analyzing, maintaining and transcompiling firewalls (WP3) IMT, UNIPI
Bodei, Chiara, Ceragioli, Lorenzo, Degano, Pierpaolo, Focardi, Riccardo, Galletta, Letterio, Luccio, Flaminia, Tempesta, Mauro, Veronese, Lorenzo.
Journal of Computer Security , Volume 29, 77--134, 2021.

Mechanical incrementalization of typing algorithms (WP1) IMT, UNIPI
Busi, Matteo, Degano, Pierpaolo, Galletta, Letterio.
Science of Computer Programming , Volume 208, 102657, 2021.

Securing interruptible enclaved execution on small microprocessors (WP1) IMT, UNIPI
Busi, Matteo, Noorman, Job, Van Bulck, Jo, Galletta, Letterio, Degano, Pierpaolo, Mühlberg, Jan Tobias, Piessens, Frank.
ACM Transactions on Programming Languages and Systems (TOPLAS) , Volume 43, 1--77, 2021.

Modelling and analysing IoT systems (WP1) IMT, UNIPI
Bodei, Chiara, Degano, Pierpaolo, Ferrari, Gian-Luigi, Galletta, Letterio.
Journal of Parallel and Distributed Computing , Volume 157, 233--242, 2021.

Distributed service-level agreement management with smart contracts and blockchain (WP1) IMT
Rafael Brundo Uriarte, Huan Zhou, Kyriakos Kritikos, Zeshun Shi, Zhiming Zhao, Rocco De Nicola.
Concurr. Comput. Pract. Exp. , Volume 33, 2021.

Automated Replication of Tuple Spaces via Static Analysis (WP1, WP2) GSSI
De Nicola, Rocco, Omar Inverso, Aline Uwimbabazi.
Fundamentals of Software Engineering (FSEN) [to appear]. LNCS, 2021.

A Coinductive Version of Milner's Proof System for Regular Expressions Modulo Bisimilarity (WP1) GSSI
Clemens Grabmayer.
9th Conference on Algebra and Coalgebra in Computer Science [to appear]. LIPIcs, 2021.

Towards Probabilistic Session-Type Monitoring (WP1, WP3, WP4) GSSI
Christian Bartolo Burlò, Adrian Francalanza, Alceste Scalas, Catia Trubiani, Emilio Tuosto.
Editors Ferruccio Damiani, Ornela Dardha.
Coordination Models and Languages - 23rd {IFIP} {WG} 6.1 International Conference, {COORDINATION} 2021, Held as Part of the 16th International Federated Conference on Distributed Computing Techniques, DisCoTec 2021, Valletta, Malta, June 14-18, 2021, Proceedings. Lecture Notes in Computer Science, Volume 12717, 106--120, 2021.

The Best a Monitor Can Do (WP4) GSSI
Luca Aceto, Antonis Achilleos, Adrian Francalanza, Anna Ingólfsdóttir, Karoliina Lehtinen.
Editors Christel Baier, Jean Goubault-Larrecq.
29th {EACSL} Annual Conference on Computer Science Logic, {CSL} 2021, January 25-28, 2021, Ljubljana, Slovenia (Virtual Conference). LIPIcs, Volume 183, 7:1--7:23, 2021.

Better Late Than Never or: Verifying Asynchronous Components at Runtime (WP4) GSSI
Duncan Paul Attard, Luca Aceto, Antonis Achilleos, Adrian Francalanza, Anna Ingólfsdóttir, Karoliina Lehtinen.
Editors Kirstin Peters, Tim A. C. Willemse.
Formal Techniques for Distributed Objects, Components, and Systems - 41st {IFIP} {WG} 6.1 International Conference, {FORTE} 2021, Held as Part of the 16th International Federated Conference on Distributed Computing Techniques, DisCoTec 2021, Valletta, Malta, June 14-18, 2021, Proceedings. Lecture Notes in Computer Science, Volume 12719, 207--225, 2021.

Bounded Verification of Multi-Threaded Programs via Lazy Sequentialization (WP2, WP3) GSSI
O. Inverso, E. Tomasco, B. Fischer, S. La Torre, G. Parlato.
ACM TOPLAS [to appear] , 2021.

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

2020

Lambda-Symsym: An Interactive Tool for Playing with Involutions and Types (WP3) UNIUD
Furio Honsell, Marina Lenisa, Ivan Scagnetto.
Editors Ugo de'Liguoro, Stefano Berardi, Thorsten Altenkirch.
26th International Conference on Types for Proofs and Programs, {TYPES} 2020, March 2-5, 2020, University of Turin, Italy. LIPIcs, Volume 188, 7:1--7:18, 2020.

Towards a Formal Model for Composable Container Systems (WP1, WP2, WP5) UNIUD
Burco, Fabio, Miculan, Marino, Peressotti, Marco.
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, Hernán C. Melgratti, Christian Roldán, Matteo Sammartino.
Editors Violet Ka I Pun, Volker Stolz, Adenilso Simão.
Theoretical Aspects of Computing - {ICTAC} 2020 - 17th International Colloquium, Macau, China, November 30 - December 4, 2020, Proceedings. Lecture Notes in Computer Science, Volume 12545, 283--303, 2020.

A comparison of NLP Tools for RE to extract Variation Points (WP3) UNIPI
Monica Arrabito, Alessandro Fantechi, Stefania Gnesi, Laura Semini.
Joint Proceedings of {REFSQ-2020} Workshops, Doctoral Symposium, Live Studies Track, and Poster Track co-located with the 26th International Conference on Requirements Engineering: Foundation for Software Quality (REFSQ 2020), Pisa, Italy, March 24, 2020. {CEUR} Workshop Proceedings, Volume 2584, 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.

MoonLight: {A} Lightweight Tool for Monitoring Spatio-Temporal Properties (WP2) UNICAM
Ezio Bartocci, Luca Bortolussi, Michele Loreti, Laura Nenzi, Simone Silvetti.
Editors Jyotirmoy Deshmukh, Dejan Nickovic.
Runtime Verification - 20th International Conference, {RV} 2020, Los Angeles, CA, USA, October 6-9, 2020, Proceedings. Lecture Notes in Computer Science, Volume 12399, 417--428, 2020.

Fluid approximation of broadcasting systems (WP2) UNICAM
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) IMT, UNICAM
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 Violet K.I. Pun, Adenilso Simao, Volker Stolz.
Proceedings of the 17th International Colloquium on Theoretical Aspects of Computing (ICTAC'20). Lecture Notes in Computer Science, Volume 12545, 200-220, 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'20). Lecture Notes in Computer Science, Volume 12478, 467-485, 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'20). Lecture Notes in Computer Science, Volume 12476, 368-384, 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'20). 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'20), 11:1-11:9, 2020.

Strategy Synthesis for Autonomous Driving in a Moving Block Railway System with Uppaal Stratego (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'20). 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'20). 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'20). 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, 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.
CoRR , Volume abs/2005.05578, 2020.
Open Access: arXiv is open access

Rigorous Engineering of Collective Adaptive Systems Introduction to the 3rd Track Edition (WP1, WP3) IMT
Martin Wirsing, Rocco De Nicola and* Stefan Jähnichen.
ISoLA {(2)}. Lecture Notes in Computer Science, Volume 12477, 161--170, 2020.

Verifying AbC Specifications via Emulation (WP1, WP3) IMT, GSSI
Rocco De Nicola, Tan Duong, Omar Inverso.
ISoLA (2). Lecture Notes in Computer Science, Volume 12477, 261--279, 2020.

{PALM:} {A} Technique for Process ALgebraic Specification Mining (WP1) IMT, UNICAM
Sara Belluccini, Rocco De Nicola, Barbara Re, Francesco Tiezzi.
{IFM}. Lecture Notes in Computer Science, Volume 12546, 397--418, 2020.

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 (WP3, WP5) 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.

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.

Composing Communicating Systems, Synchronously (WP1) GSSI
Franco Barbanera, Ivan Lanese, Emilio Tuosto.
Editors Tiziana Margaria, Bernhard Steffen.
Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20-30, 2020. Lecture Notes in Computer Science, Volume 12476, 39--59, 2020.

On Testing Message-Passing Components (WP2, WP3) GSSI
Alex Coto, Roberto Guanciale, Emilio Tuosto.
Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20-30, 2020. Lecture Notes in Computer Science, Volume 12476, 22-38, 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.

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

Tight Error Analysis in Fixed-point Arithmetics (WP3) GSSI, IMT
Stella Simic, Alberto Bemporad, Omar Inverso, Mirco Tribastone.
Editors Brijesh Dongol, Elena Troubitsyna.
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.

Abstractions for Collective Adaptive Systems (WP1, WP4) GSSI
Omar Inverso, Catia Trubiani, Emilio Tuosto.
Editors Tiziana Margaria, Bernhard Steffen.
Leveraging Applications of Formal Methods, Verification and Validation: Engineering Principles - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20-30, 2020, Proceedings, Part {II}. Lecture Notes in Computer Science, Volume 12477, 243--260, 2020.

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

Combining SLiVER with CADP to Analyze Multi-agent Systems (WP2, 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.

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

An Abstract Framework for Choreographic Testing (WP3, WP4) GSSI
Alex Coto, Roberto Guanciale, Emilio Tuosto.
ICE 2020, Volume abs/2009.07990, 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.

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, Hernán C. Melgratti, Christian Roldán, Matteo Sammartino.
Editors Arkadev Chattopadhyay, Paul Gastin.
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.

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.

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

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