An Interactive Debugger for a Concurrent Language. - Nicoletta De Francesco; Diego Latella; Gigliola Vaglini (ICSE, 1985)

Shared Abstract Data Types: An Algebraic Methodology for Their Specification. - Andrea Bondavalli; Nicoletta De Francesco; Diego Latella; Gigliola Vaglini (MFDBS, 1989)

Techniques for the formal definition of the G-LOTOS syntax. - Tommaso Bolognesi; Diego Latella (VL, 1989)

Non-standard Interpretations of LOTOS Specifications. - Tommaso Bolognesi; Diego Latella; Elisabetta Zuppa (TAPSOFT, Vol.2, 1991)

The Definition of a Graphical G-LOTOS Editor Using the Meta-Tool LOGGIE. - Tommaso Bolognesi; Olof Hagsand; Diego Latella; Björn Pehrson (Comput. Networks ISDN Syst., 1991)

Using Abstract Interpretation for Gate splitting in LOTOS Specifications. - Fosca Giannotti; Diego Latella (WSA, 1992)

Modeling Systems by Probabilistic Process Algebra: an Event Structures Approach. - Joost-Pieter Katoen; Rom Langerak; Diego Latella (FORTE, 1993)

A Fully Parallel Calculus of Synchronizing Processes. - Diego Latella; Paola Quaglia (TAPSOFT, 1993)

Gate Splitting in LOTOS Specifications Using Abstract Interpretation. - Fosca Giannotti; Diego Latella (Sci. Comput. Program., 1994)

A Stochastic Causality-Based Process Algebra. - Ed Brinksma; Joost-Pieter Katoen; Rom Langerak; Diego Latella (Comput. J., 1995)

Towards Automatic Temporal Logic Verification of Value Passing Process Algebra Using Abstract Interpretation. - Alessandro Fantechi; Stefania Gnesi; Diego Latella (CONCUR, 1996)

On Specifying Real-Time Systems in a Causality-Based Setting. - Joost-Pieter Katoen; Rom Langerak; Diego Latella; Ed Brinksma (FTRTFT, 1996)

Partial Order Models for Quantitative Extensions of LOTOS. - Ed Brinksma; Joost-Pieter Katoen; Rom Langerak; Diego Latella (Comput. Networks, 1998)

Automatic Verification of a Lip-Synchronisation Protocol Using Uppaal. - Howard Bowman; Giorgio P. Faconti; Joost-Pieter Katoen; Diego Latella; Mieke Massink (Formal Aspects Comput., 1998)

Editorial. - Stefania Gnesi; Diego Latella (Formal Aspects Comput., 1998)

Special Issue on the First International workshop of the ERCIM Working Group on Formal Methods for Industrial Critical Systems, St. Hugh's College, Oxford, March 19, 1996 - Selected Papers. - Stefania Gnesi; Diego Latella (Formal Methods Syst. Des., 1998)

A Consistent Causality-Based View on a Timed Process Algebra Including Urgent Interactions. - Joost-Pieter Katoen; Rom Langerak; Ed Brinksma; Diego Latella; Tommaso Bolognesi (Formal Methods Syst. Des., 1998)

Towards a Formal Operational Semantics of UML Statechart Diagrams. - Diego Latella; István Majzik; Mieke Massink (FMOODS, 1999)

Model Checking UML Statechart Diagrams Using JACK. - Stefania Gnesi; Diego Latella; Mieke Massink (HASE, 1999)

High-level Integrated Design Environment for dependability (HIDE). - Andrea Bondavalli; Mario Dal Cin; Diego Latella; András Pataricza (WORDS (Fall), 1999)

Automatic Verification of a Behavioural Subset of UML Statechart Diagrams Using the SPIN Model-checker. - Diego Latella; István Majzik; Mieke Massink (Formal Aspects Comput., 1999)

An Automatic SPIN Validation of a Safety Critical Railway Control System. - Stefania Gnesi; Diego Latella; Gabriele Lenzini; C. Abbaneo; Arturo M. Amendola; P. Marmo (DSN, 2000)

A stochastic extension of a behavioural subset of UML statechart diagrams. - Stefania Gnesi; Diego Latella; Mieke Massink (HASE, 2000)

A Formal Specification and Validation of a Critical System in Presence of Byzantine Errors. - Stefania Gnesi; Diego Latella; Gabriele Lenzini; C. Abbaneo; Arturo M. Amendola; P. Marmo (TACAS, 2000)

Foreword. - Jorge Cuéllar; Stefania Gnesi; Diego Latella (Sci. Comput. Program., 2000)

A Formal Testing Framework for UML Statechart Diagrams Behaviours: From Theory to Automatic Verification. - Diego Latella; Mieke Massink (HASE, 2001)

First Passage Time Analysis of Stochastic Process Algebra Using Partial Orders. - Theo C. Ruys; Rom Langerak; Joost-Pieter Katoen; Diego Latella; Mieke Massink (TACAS, 2001)

Dependability analysis in the early phases of UML-based system design. - Andrea Bondavalli; Mario Dal Cin; Diego Latella; István Majzik; András Pataricza; Giancarlo Savoia (Comput. Syst. Sci. Eng., 2001)

Introduction: Special Issue on the Fourth International Workshop of the ERCIM Working Group on Formal Methods for Industrial Critical Systems, Trento, July 11-12, 1999 - Selected Papers. - Stefania Gnesi; Diego Latella (Formal Methods Syst. Des., 2001)

Design Validation of Embedded Dependable Systems. - Andrea Bondavalli; Alessandro Fantechi; Diego Latella; Luca Simoncini (IEEE Micro, 2001)

Metric semantics for true concurrent real time. - Joost-Pieter Katoen; Christel Baier; Diego Latella (Theor. Comput. Sci., 2001)

On testing and conformance relations for UML statechart diagrams behaviours. - Diego Latella; Mieke Massink (ISSTA, 2002)

AGILE: Software Architecture for Mobility. - Luís Andrade 001; Paolo Baldan; Hubert Baumeister; Roberto Bruni 001; Andrea Corradini 001; Rocco De Nicola; José Luiz Fiadeiro; Fabio Gadducci; Stefania Gnesi; Piotr Hoffman; Nora Koch; Piotr Kosiuczenko; et al. (WADT, 2002)

Modular semantics for a UML statechart diagrams kernel and its extension to multicharts and branching time model-checking. - Stefania Gnesi; Diego Latella; Mieke Massink (J. Log. Algebraic Methods Program., 2002)

On Mobility Extensions of UML Statecharts. A Pragmatic Approach. - Diego Latella; Mieke Massink (FMOODS, 2003)

Model Checking Groupware Protocols. - Maurice H. ter Beek; Mieke Massink; Diego Latella; Stefania Gnesi (COOP, 2004)

Model Checking Dependability Attributes of Wireless Group Communication. - Mieke Massink; Joost-Pieter Katoen; Diego Latella (DSN, 2004)

Mobile UML Statecharts with Localities. - Diego Latella; Mieke Massink; Hubert Baumeister; Martin Wirsing (Global Computing, 2004)

Formal Test-Case Generation for UML Statecharts. - Stefania Gnesi; Diego Latella; Mieke Massink (ICECCS, 2004)

Model Checking Publish/Subscribe Notification for thinkteam®. - Maurice H. ter Beek; Mieke Massink; Diego Latella; Stefania Gnesi; Alessandro Forghieri; Maurizio Sebastianis (FMICS, 2004)

Towards Model Checking Stochastic Aspects of the thinkteam User Interface. - Maurice H. ter Beek; Mieke Massink; Diego Latella (DSV-IS, 2005)

A case study on the automated verification of groupware protocols. - Maurice H. ter Beek; Mieke Massink; Diego Latella; Stefania Gnesi; Alessandro Forghieri; Maurizio Sebastianis (ICSE, 2005)

Formal modeling and quantitative analysis of KLAIM-based mobile systems. - Rocco De Nicola; Diego Latella; Mieke Massink (SAC, 2005)

Towards a Logic for Performance and Mobility. - Rocco De Nicola; Joost-Pieter Katoen; Diego Latella; Mieke Massink (QAPL, 2005)

On testing UML statecharts. - Mieke Massink; Diego Latella; Stefania Gnesi (J. Log. Algebraic Methods Program., 2006)

Model checking mobile stochastic logic. - Rocco De Nicola; Joost-Pieter Katoen; Diego Latella; Michele Loreti; Mieke Massink (Theor. Comput. Sci., 2007)

A Fluid Flow Approach to Usability Analysis of Multi-user Systems. - Mieke Massink; Diego Latella; Maurice H. ter Beek; Michael D. Harrison; Michele Loreti (TAMODIA/HCSE, 2008)

Combining Timed Coordination Primitives and Probabilistic Tuple Spaces. - Mario Bravetti; Diego Latella; Michele Loreti; Mieke Massink; Gianluigi Zavattaro (TGC, 2008)

MarCaSPiS: a Markovian Extension of a Calculus for Services. - Rocco De Nicola; Diego Latella; Michele Loreti; Mieke Massink (SOS@ICALP, 2008)

Assisting the Design of an Industrial Groupware System by Model Checking. - Maurice H. ter Beek; Stefania Gnesi; Diego Latella; Mieke Massink; Maurizio Sebastianis; Gianluca Trentanni (ERCIM News, 2008)

Engineering crowd interaction within smart environments. - Michael D. Harrison; Mieke Massink; Diego Latella (EICS, 2009)

On a Uniform Framework for the Definition of Stochastic Process Languages. - Rocco De Nicola; Diego Latella; Michele Loreti; Mieke Massink (FMICS, 2009)

Rate-Based Transition Systems for Stochastic Process Calculi. - Rocco De Nicola; Diego Latella; Michele Loreti; Mieke Massink (ICALP (2), 2009)

Assisting the design of a groupware system. - Maurice H. ter Beek; Stefania Gnesi; Diego Latella; Mieke Massink; Maurizio Sebastianis; Gianluca Trentanni (J. Log. Algebraic Methods Program., 2009)

Reconciling Population and Agent Models for Crowd Dynamics. - Andrea Bracciali; Jane Hillston; Diego Latella; Mieke Massink (LAM@LICS, 2010)

Scalable analysis of collective behaviour in smart service systems. - Mieke Massink; Michael D. Harrison; Diego Latella (SAC, 2010)

A Scalable Fluid Flow Process Algebraic Approach to Emergency Egress Analysis. - Mieke Massink; Diego Latella; Andrea Bracciali; Michael D. Harrison (SEFM, 2010)

Quantitative Analysis of Services. - Igor Cappello; Allan Clark; Stephen Gilmore; Diego Latella; Michele Loreti; Paola Quaglia; Stefano Schivo (Results of the SENSORIA Project, 2011)

SoSL: A Service-Oriented Stochastic Logic. - Rocco De Nicola; Diego Latella; Michele Loreti; Mieke Massink (Results of the SENSORIA Project, 2011)

Modelling Non-linear Crowd Dynamics in Bio-PEPA. - Mieke Massink; Diego Latella; Andrea Bracciali; Jane Hillston (FASE, 2011)

Analysing Robot Swarm Decision-Making with Bio-PEPA. - Mieke Massink; Manuele Brambilla; Diego Latella; Marco Dorigo; Mauro Birattari (ANTS, 2012)

Fluid Analysis of Foraging Ants. - Mieke Massink; Diego Latella (COORDINATION, 2012)

Bisimulation of Labeled State-to-Function Transition Systems of Stochastic Process Languages - Diego Latella; Mieke Massink; Erik P. de Vink (ACCAT, 2012)

Scalable context-dependent analysis of emergency egress models. - Mieke Massink; Diego Latella; Andrea Bracciali; Michael D. Harrison; Jane Hillston (Formal Aspects Comput., 2012)

Stochastic Process Algebra and Stability Analysis of Collective Systems. - Luca Bortolussi; Diego Latella; Mieke Massink (COORDINATION, 2013)

On-the-fly Fast Mean-Field Model-Checking. - Diego Latella; Michele Loreti; Mieke Massink (TGC, 2013)

On-the-fly Fast Mean-Field Model-Checking: Extended Version. - Diego Latella; Michele Loreti; Mieke Massink (CoRR, 2013)

A uniform definition of stochastic process calculi. - Rocco De Nicola; Diego Latella; Michele Loreti; Mieke Massink (ACM Comput. Surv., 2013)

Continuous approximation of collective system behaviour: A tutorial. - Luca Bortolussi; Jane Hillston; Diego Latella; Mieke Massink (Perform. Evaluation, 2013)

On the use of Bio-PEPA for modelling and analysing collective behaviours in swarm robotics. - Mieke Massink; Manuele Brambilla; Diego Latella; Marco Dorigo; Mauro Birattari (Swarm Intell., 2013)

Specifying and Verifying Properties of Space. - Vincenzo Ciancia; Diego Latella; Michele Loreti; Mieke Massink (IFIP TCS, 2014)

Data Verification for Collective Adaptive Systems: Spatial Model-Checking of Vehicle Location Data. - Vincenzo Ciancia; Stephen Gilmore; Diego Latella; Michele Loreti; Mieke Massink (SASO Workshops, 2014)

Specifying and Verifying Properties of Space - Extended Version. - Vincenzo Ciancia; Diego Latella; Michele Loreti; Mieke Massink (CoRR, 2014)

On-the-fly Probabilistic Model Checking. - Diego Latella; Michele Loreti; Mieke Massink (ICE, 2014)

Stochastically timed predicate-based communication primitives for autonomic computing. - Diego Latella; Michele Loreti; Mieke Massink; Valerio Senni (QAPL, 2014)

A Quantitative Approach to the Design and Analysis of Collective Adaptive Systems for Smart Cities. - Maurice H. ter Beek; Luca Bortolussi; Vincenzo Ciancia; Stefania Gnesi; Jane Hillston; Diego Latella; Mieke Massink (ERCIM News, 2014)

On StocS: A Stochastic Extension of SCEL. - Diego Latella; Michele Loreti; Mieke Massink; Valerio Senni (Software, Services, and Systems, 2015)

Investigating Fluid-Flow Semantics of Asynchronous Tuple-Based Process Languages for Collective Adaptive Systems. - Diego Latella; Michele Loreti; Mieke Massink (COORDINATION, 2015)

On-the-fly Fluid Model Checking via Discrete Time Population Models. - Diego Latella; Michele Loreti; Mieke Massink (EPEW, 2015)

Exploring Spatio-temporal Properties of Bike-Sharing Systems. - Vincenzo Ciancia; Diego Latella; Mieke Massink; Rytis Paskauskas (SASO Workshops, 2015)

Towards Automatic Decision Support for Bike-Sharing System Design. - Maurice H. ter Beek; Stefania Gnesi; Diego Latella; Mieke Massink (SEFM Workshops, 2015)

An Experimental Spatio-Temporal Model Checker. - Vincenzo Ciancia; Gianluca Grilletti; Diego Latella; Michele Loreti; Mieke Massink (SEFM Workshops, 2015)

CARMA: Collective Adaptive Resource-sharing Markovian Agents. - Luca Bortolussi; Rocco De Nicola; Vashti Galpin; Stephen Gilmore; Jane Hillston; Diego Latella; Michele Loreti; Mieke Massink (QAPL, 2015)

A Definition Scheme for Quantitative Bisimulation. - Diego Latella; Mieke Massink; Erik P. de Vink (QAPL, 2015)

Bisimulation of Labelled State-to-Function Transition Systems Coalgebraically. - Diego Latella; Mieke Massink; Erik P. de Vink (Log. Methods Comput. Sci., 2015)

On-the-fly PCTL fast mean-field approximated model-checking for self-organising coordination. - Diego Latella; Michele Loreti; Mieke Massink (Sci. Comput. Program., 2015)

The SCEL Language: Design, Implementation, Verification. - Rocco De Nicola; Diego Latella; Alberto Lluch-Lafuente; Michele Loreti; Andrea Margheri; Mieke Massink; Andrea Morichetta 001; Rosario Pugliese; Francesco Tiezzi 001; Andrea Vandin (The ASCENS Approach, 2015)

On-the-Fly Mean-Field Model-Checking for Attribute-Based Coordination. - Vincenzo Ciancia; Diego Latella; Mieke Massink (COORDINATION, 2016)

A Tool-Chain for Statistical Spatio-Temporal Model Checking of Bike Sharing Systems. - Vincenzo Ciancia; Diego Latella; Mieke Massink; Rytis Paskauskas; Andrea Vandin (ISoLA (1), 2016)

Spatial Logic and Spatial Model Checking for Closure Spaces. - Vincenzo Ciancia; Diego Latella; Michele Loreti; Mieke Massink (SFM, 2016)

From Collective Adaptive Systems to Human Centric Computation and Back: Spatial Model Checking for Medical Imaging. - Gina Belmonte; Vincenzo Ciancia; Diego Latella; Mieke Massink (FORECAST@STAF, 2016)

Model Checking Spatial Logics for Closure Spaces. - Vincenzo Ciancia; Diego Latella; Michele Loreti; Mieke Massink (Log. Methods Comput. Sci., 2016)

On Formal Methods for Collective Adaptive System Engineering. {Scalable Approximated, Spatial} Analysis Techniques. Extended Abstract. - Diego Latella (FORECAST@STAF, 2016)

FlyFast: A Scalable Approach to Probabilistic Model-Checking Based on Mean-Field Approximation. - Diego Latella; Michele Loreti; Mieke Massink (ModelEd, TestEd, TrustEd, 2017)

FlyFast: A Mean Field Model Checker. - Diego Latella; Michele Loreti; Mieke Massink (TACAS (2), 2017)

Design and Optimisation of the FlyFast Front-end for Attribute-based Coordination. - Diego Latella; Mieke Massink (QAPL@ETAPS, 2017)

VoxLogicA: a Spatial Model Checker for Declarative Image Analysis (Extended Version). - Gina Belmonte; Vincenzo Ciancia; Diego Latella; Mieke Massink (CoRR, 2018)

Spatial Logics and Model Checking for Medical Imaging (Extended Version). - Fabrizio Banci Buonamici; Gina Belmonte; Vincenzo Ciancia; Diego Latella; Mieke Massink (CoRR, 2018)

A refined mean field approximation of synchronous discrete-time population models. - Nicolas Gast; Diego Latella; Mieke Massink (Perform. Evaluation, 2018)

A Refined Mean Field Approximation for Synchronous Population Processes. - Nicolas Gast; Diego Latella; Mieke Massink (SIGMETRICS Perform. Evaluation Rev., 2018)

Spatio-temporal model checking of vehicular movement in public transport systems. - Vincenzo Ciancia; Stephen Gilmore; Gianluca Grilletti; Diego Latella; Michele Loreti; Mieke Massink (Int. J. Softw. Tools Technol. Transf., 2018)

Innovating Medical Image Analysis via Spatial Logics. - Gina Belmonte; Vincenzo Ciancia; Diego Latella; Mieke Massink (From Software Engineering to Formal Methods and Tools, and Back, 2019)

Embedding RCC8D in the Collective Spatial Logic CSLCS. - Vincenzo Ciancia; Diego Latella; Mieke Massink (Models, Languages, and Tools for Concurrent and Distributed Programming, 2019)

VoxLogicA: A Spatial Model Checker for Declarative Image Analysis. - Gina Belmonte; Vincenzo Ciancia; Diego Latella; Mieke Massink (TACAS (1), 2019)

VoxLogicA: a Spatial-Logic Based Tool for Declarative Image Analysis. - Gina Belmonte; Vincenzo Ciancia; Diego Latella; Mieke Massink (ERCIM News, 2019)

Refined Mean Field Analysis: The Gossip Shuffle Protocol Revisited. - Nicolas Gast; Diego Latella; Mieke Massink (COORDINATION, 2020)

Refined Mean Field Analysis of the Gossip Shuffle Protocol - extended version -. - Nicolas Gast; Diego Latella; Mieke Massink (CoRR, 2020)

Towards Spatial Bisimilarity for Closure Models: Logical and Coalgebraic Characterisations. - Vincenzo Ciancia; Diego Latella; Mieke Massink; Erik P. de Vink (CoRR, 2020)

Using Spatial Logic and Model Checking for Nevus Segmentation. - Gina Belmonte; Giovanna Broccia; Vincenzo Ciancia; Diego Latella; Mieke Massink (CoRR, 2020)

Spatial logics and model checking for medical imaging. - Fabrizio Banci Buonamici; Gina Belmonte; Vincenzo Ciancia; Diego Latella; Mieke Massink (Int. J. Softw. Tools Technol. Transf., 2020)

Towards Model Checking Video Streams Using VoxLogicA on GPUs. - Laura Bussi; Vincenzo Ciancia; Fabio Gadducci; Diego Latella; Mieke Massink (DataMod, 2021)

Spatial Model Checking for Smart Stations - Research Challenges. - Maurice H. ter Beek; Vincenzo Ciancia; Diego Latella; Mieke Massink; Giorgio Oronzo Spagnolo (FMICS, 2021)

Feasibility of Spatial Model Checking for Nevus Segmentation. - Gina Belmonte; Giovanna Broccia; Vincenzo Ciancia; Diego Latella; Mieke Massink (FormaliSE@ICSE, 2021)

Querying Medical Imaging Datasets Using Spatial Logics (Position Paper). - Gina Belmonte; Giovanna Broccia; Laura Bussi; Vincenzo Ciancia; Diego Latella; Mieke Massink (MEDI Workshops, 2021)

A Hands-On Introduction to Spatial Model Checking Using VoxLogicA - - Invited Contribution. - Vincenzo Ciancia; Gina Belmonte; Diego Latella; Mieke Massink (SPIN, 2021)

On Bisimilarities for Closure Spaces - Preliminary Version. - Vincenzo Ciancia; Diego Latella; Mieke Massink; Erik P. de Vink (CoRR, 2021)

Back-and-Forth in Space: On Logics and Bisimilarity in Closure Spaces. - Vincenzo Ciancia; Diego Latella; Mieke Massink; Erik P. de Vink (A Journey from Process Algebra via Timed Automata to Model Learning, 2022)

Towards a GUI for Declarative Medical Image Analysis: Cognitive and Memory Load Issues. - Giovanna Broccia; Vincenzo Ciancia; Diego Latella; Mieke Massink (HCI (38), 2022)

On Binding in the Spatial Logics for Closure Spaces. - Laura Bussi; Vincenzo Ciancia; Fabio Gadducci; Diego Latella; Mieke Massink (ISoLA (1), 2022)

Geometric Model Checking of Continuous Space. - Nick Bezhanishvili; Vincenzo Ciancia; David Gabelaia; Gianluca Grilletti; Diego Latella; Mieke Massink (Log. Methods Comput. Sci., 2022)

Minimisation of Spatial Models Using Branching Bisimilarity. - Vincenzo Ciancia; Jan Friso Groote; Diego Latella; Mieke Massink; Erik P. de Vink (FM, 2023)

On Bisimilarity for Polyhedral Models and SLCS. - Vincenzo Ciancia; David Gabelaia; Diego Latella; Mieke Massink; Erik P. de Vink (FORTE, 2023)

On Bisimilarity for Quasi-discrete Closure Spaces. - Vincenzo Ciancia; Diego Latella; Mieke Massink; Erik P. de Vink (CoRR, 2023)

Measured Causes: Adding Time and Probability to True Concurrency - Ten Papers with Pisa and Twente. - Ed Brinksma; Rom Langerak; Diego Latella; Mieke Massink (Principles of Verification (3), 2024)

Weak Simplicial Bisimilarity for Polyhedral Models and SLCSη. - Nick Bezhanishvili; Vincenzo Ciancia; David Gabelaia; Mamuka Jibladze; Diego Latella; Mieke Massink; Erik P. de Vink (FORTE, 2024)

Towards Hybrid-AI in Imaging Using VoxLogicA. - Gina Belmonte; Laura Bussi; Vincenzo Ciancia; Diego Latella; Mieke Massink (ISoLA (4), 2024)

Weak Simplicial Bisimilarity for Polyhedral Models and SLCS_eta - Extended Version. - Nick Bezhanishvili; Vincenzo Ciancia; David Gabelaia; Mamuka Jibladze; Diego Latella; Mieke Massink; Erik P. de Vink (CoRR, 2024)

Weak Simplicial Bisimilarity and Minimisation for Polyhedral Model Checking. - Nick Bezhanishvili; Laura Bussi; Vincenzo Ciancia; David Gabelaia; Mamuka Jibladze; Diego Latella; Mieke Massink; Erik P. de Vink (CoRR, 2024)

Ten Years of Spatial Model Checking. - Vincenzo Ciancia; Diego Latella; Mieke Massink (Rebeca for Actor Analysis in Action, 2025)

Practical Exploration of Polyhedral Model Checking. - Yuri Andriaccio; Vincenzo Ciancia; Diego Latella; Mieke Massink (CoRR, 2025)