Lizzit, Michele ; Pinzauti, Francesco ; Miculan, Marino ; Riccio, Vincenzo: Security Assessment of Private Package Repositories: An Experience on Acc-Py at CERN. In: Journal of Software: Evolution and Process vols. 38 (2026), Nr. 8, p. e70159
The introduction of package managers had a huge impact on software development, as they facilitate dependency management and the access to reusable code components. However, reliance on centralized repositories introduces security risks, as they are increasingly exploited in supply chain attacks. To reduce these risks, many companies rely on private package managers and repositories. Although public package repositories have been extensively studied, private ones remain underexplored. This paper presents a security comparison of private package repositories versus their public counterparts, through our experience on PyPI and CERN’s Acc-Py. We perform a comprehensive security assessment of both repositories, complemented by discussions with the CERN development team. Using open-source static analyzers, we find that Acc-Py hosts packages with fewer potential security issues than those on the broad PyPI ecosystem. However, it remains susceptible to dependency confusion attacks due to namespace collisions with PyPI. Our dynamic analysis technique identifies telemetry collection as a privacy-monitoring trade-off. Our study provides valuable insights for analyzing and strengthening the security of private repositories, addressing their unique security challenges and attack surfaces.
Miculan, Marino ; Paier, Matteo ; Plozner, Jacopo: Experimental Evaluation of Lightweight Encryption Algorithms on 16-bit Microcontrollers. In: Proceedings of the 23rd International Conference on Security and Cryptography - SECRYPT : SciTePress, 2026
The Internet of Things (IoT) increasingly relies on resource-constrained devices that require efficient symmetric encryption. Lightweight cryptography (LWC) addresses this by providing algorithms optimized for minimal computational and energy overhead. However, the performance of any cryptographic primitive is highly architecture-dependent, and direct experimental data on microcontrollers remains scarce in the literature. In this paper we present a rigorous evaluation of ten lightweight encryption algorithms — seven block ciphers (AES, CLEFIA, LEA, PRINCE, QARMAv2, SPARX, SPECK) and three stream ciphers (Ascon, ChaCha20, Hummingbird-2) — running on the 16-bit Texas Instruments MSP430FR6989 microcontroller, a platform widely used in industrial IoT and smart metering. Unlike prior surveys that rely solely on software counters or emulation, our methodology employs professional-grade instrumentation for real-time current profiling at the hardware level. Each algorithm is characterised under two compiler optimisation profiles (speed-optimised and size-optimised) across three metrics: encryption throughput, code footprint, and charge consumption. Our results show that ARX-based ciphers — particularly LEA and SPECK 32/64 — achieve the best energy efficiency, outperforming AES by up to 25% in charge consumption while maintaining a significantly smaller code footprint. Hardware-oriented designs (PRINCE, QARMAv2) perform poorly in software, confirming that hardware efficiency does not translate to software performance. Among stream ciphers, Ascon — the NIST LWC standard — offers the best balance of security and efficiency, whereas ChaCha20 proves unsuitable for heavily resource-constrained contexts. We provide concrete algorithm recommendations for developers targeting MSP430 and similar 16-bit platforms, and we openly release all benchmark implementations.
Baldo, Massimiliano ; Paier, Matteo ; Miculan, Marino: Policy Automata for Stateful Authorization. In: Proceedings of the 27th Italian Conference on Theoretical Computer Science (ICTCS 2026), CEUR Workshop Proceedings. vols. 4269 : CEUR-WS.org, 2026
Pasqua, Michele ; Miculan, Marino: Attribute-based memory updates with priorities for collective adaptive systems. In: International Journal on Software Tools for Technology Transfer (2026)
Miculan, Marino: KLAIM, Certified: Mechanising Flow Logic for Tuple-Space Coordination. In: Journal of Logical and Algebraic Methods in Programming (2026), p. 101179
Paier, Matteo ; Van Eeden, Roberto L. G. ; Miculan, Marino: Formal modelling and verifying eIDAS multi-factor authentication with interface-based threat analysis. In: Software and Systems Modeling (2026)
This paper introduces a methodology for the formal modelling and verification of multi-factor authentication (MFA) schemes utilized in eIDAS digital identity cards. Our approach employs an interface-based threat model to systematically analyse potential vulnerabilities and enumerate a range of threat scenarios based on varying attacker capabilities. We demonstrate the automated generation of ProVerif models for these scenarios using the Italian Carta di Identità Elettronica (CIE), an eIDAS-compliant digital identity card, as a practical case study. Our analysis reveals several security weaknesses; notably, an attacker possessing only Level 1 (i.e. single-factor) credentials can, in certain circumstances, achieve Level 2 multi-factor authentication without needing to compromise any communication interface. To mitigate these vulnerabilities, we propose minor modifications to the protocols. Furthermore, at Level 3, our analysis shows that the authentication scheme relying on the CieID smartphone application presents a broader attack surface compared to the method employing a PC with a smart card reader. The interface-based modelling and analysis methodology presented in this work offers a valuable framework that can be adapted for the security assessment of other eIDAS digital identity cards.
Baldo, Massimiliano ; Di Gianantonio, Pietro ; Paier, Matteo ; Miculan, Marino: Strobilus: Enriching Cedar with Stateful Policies. In: Proceedings of the 31st ACM Symposium on Access Control Models and Technologies (SACMAT ’26) : Association for Computing Machinery, 2026 — ISBN 979-8-4007-2107-6, pp. 205–216
Authorization is a fundamental problem in modern distributed systems, and the “policies-as-code” paradigm has emerged as a promising solution to decouple access control logic from application code. However, most policy languages lack the ability to handle stateful policies directly. This limitation forces developers to manage policy-related state within the application code, reintroducing the very coupling that policies as code aims to eliminate and opening the door to security vulnerabilities. To address this gap, we introduce Strobilus, a language designed to express effects over policy-specific data. Strobilus is built to seamlessly complement and integrate with Amazon’s Cedar, allowing developers to write stateful policies without modifying Cedar’s core syntax or evaluation engine. Strobilus is distinguished by its formal semantics, a strong typing system, and a guarantee of termination, which facilitates rigorous analysis and verification of policies. We have developed a prototype implementation in Rust, which demonstrates that Strobilus may lead to significant performance improvements over external methods for policy data management. This approach aims to fully realizes the promise of “policies-as-code” by providing a comprehensive, safe, and verifiable solution for both stateless and stateful authorization policies.
Ejeh, Dennis Glenn ; Foresti, Gian Luca ; Miculan, Marino ; De Nardin, Axel: SA-SOINN: A Self-Adaptive Neural Network for Continuous Intrusion Detection in Dynamic Environments. In: Maiorca, D. ; Samarati, P. (eds.): Proceedings of the Joint National Conference on Cybersecurity (ITASEC & SERICS 2026), CEUR Workshop Proceedings. vols. 4198 : CEUR-WS.org, 2026
Coppo, Cristian ; Longo, Francesco ; Merlino, Giovanni ; Puliafito, Antonio ; Miculan, Marino: Automatic Verification of Security Properties in Containerized IoT Applications via Bigraphical Modeling. In: Maiorca, D. ; Samarati, P. (eds.): Proceedings of the Joint National Conference on Cybersecurity (ITASEC & SERICS 2026), CEUR Workshop Proceedings. vols. 4198 : CEUR-WS.org, 2026
Comini, Marco ; Gemolotto, Luca ; Miculan, Marino: Attribute-Based Communication over Pub/Sub: Transactional Coordination for Smart Systems. In: Ferreira, C. ; Mezzina, C. A. (eds.): 45th IFIP International Conference on Formal Techniques for Distributed Objects, Components, and Systems, FORTE 2025, Lecture Notes in Computer Science. vols. 15732 : Springer, 2025 — ISBN 978-3-031-95497-9, pp. 96–113
IoT and smart systems frequently rely on publish-subscribe (pub/sub) middlewares like MQTT or DDS. However, current coordination solutions often lack formal rigour, posing risks in mission-critical applications, or suffer from excessive complexity, hindering practical deployment and increasing the likelihood of errors. This paper addresses these challenges by integrating AbU, a recently introduced formal model based on Event-Condition-Action (ECA) rules and attribute-based communication, with standard pub/sub middlewares. We present a synchronization protocol that leverages pub/sub primitives to implement AbU’s transactional communication semantics. We prove the correctness of this protocol, demonstrating that it accurately reflects the underlying system dynamics. This integration of a formal ECA-based programming model with pub/sub offers a compelling balance between rigorous guarantees and practical applicability for coordinating IoT and smart systems.
Baldo, Massimiliano ; Ion, Fabio Ionut ; Miculan, Marino ; Paier, Matteo ; Riccio, Vincenzo: OWSM: Empowering Rego for Stateful Access Control. In: Costa, G. ; Montanari, R. ; Carminati, M. ; Sciarretta, G. (eds.): Proceedings of the Joint National Conference on Cybersecurity (ITASEC & SERICS 2025), CEUR Workshop Proceedings. vols. 3962 : CEUR-WS.org, 2025
Ejeh, Dennis Glenn ; Foresti, Gian Luca ; Miculan, Marino ; De Nardin, Axel: Real-Time Anomaly Detection in Docker Containers: A Continuous Learning Approach Using SF-SOINN. In: Costa, G. ; Montanari, R. ; Carminati, M. ; Sciarretta, G. (eds.): Proceedings of the Joint National Conference on Cybersecurity (ITASEC & SERICS 2025), CEUR Workshop Proceedings. vols. 3962 : CEUR-WS.org, 2025
Pasqua, Michele ; Miculan, Marino: Local Reasoning and Attribute-Based Memory Updates for Enforcing Global Invariants in Collective Adaptive Systems. In: Margaria, T. ; Steffen, B. (eds.): 12th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2024 : Springer, 2024 — ISBN 978-3-031-75107-3, pp. 351–367
We address the problem of enforcing global invariants, i.e., system-level properties, in Collective Adaptive Systems, such as distributed and decentralized Internet of Things (IoT) solutions. In particular, we propose a novel approach adopting Attribute-based memory Updates (AbU), a calculus modeling declarative, event-driven systems with attribute-based communication.
Costantini, Federico ; Bistarelli, Stefano ; Crisci, Francesco ; Miculan, Marino ; Piasentier, Edi: La digitalizzazione mediante blockchain della filiera CarnePRI, Tracce. Itinerari di ricerca/Area scientifica : Forum, 2024 — ISBN 978-88-3283-509-0
Paier, Matteo ; Van Eeden, Roberto ; Miculan, Marino: Formal Analysis of Multi-Factor Authentication Schemes in Digital Identity Cards. In: Madeira, A. ; Knapp, A. (eds.): International Conference on Software Engineering and Formal Methods, SEFM 2024 : Springer, 2024. — Best Paper Award — ISBN 978-3-031-77382-2, pp. 423–440
We present a methodology for formally modelling and verifying multi-factor authentication (MFA) schemes employed in eIDAS digital identity cards. This methodology adopts an interface-based threat model to comprehensively analyse potential vulnerabilities and enumerate threat scenarios based on an attacker’s capabilities. Using CIE, Italy’s eIDAS-compliant digital identity card, as guiding example, we show how to automatically generate ProVerif models of these scenarios. Our analysis exposes some vulnerabilities; e.g., an attacker with Level 1 credentials can gain Level 2 authentication, even without compromising any interface. To address these vulnerabilities, we propose minor modifications to the protocols, whose correctness is proved by further formal analysis.
Paier, Matteo ; Pizzolitto, Mattia ; Foresti, Gian Luca ; Miculan, Marino: Netstaldi: A Modular Distributed Architecture for Incremental Network Discovery. In: D’Angelo, G. ; Luccio, F. ; Palmieri, F. (eds.): Proceedings of the 8th Italian Conference on Cyber Security (ITASEC 2024), CEUR Workshop Proceedings. vols. 3731 : CEUR-WS.org, 2024
Van Eeden, Roberto ; Paier, Matteo ; Miculan, Marino: A Formal Analysis of CIE Level 2 Multi-Factor Authentication via SMS OTP. In: Proceedings of the 21st International Conference on Security and Cryptography - SECRYPT : SciTePress, 2024 — ISBN 978-989-758-709-2, pp. 483–491
We analyze the security of Level 2 multi-factor authentication (MFA) based on SMS One-Time Passcode (OTP) of Italian Electronic Identity Card (CIE). We propose a novel threat model encompassing password compromise, network disruptions, user errors, and malware attacks. The combinations of the adversary’s attack capabilites yield a plethora of possible attack scenarios, which we systematically generate, formalise and verify in ProVerif. Our analysis reveals that CIE MFA based on SMS OTP is vulnerable to attacks with read access to the mobile device or keyboard, or to phishing, but event to mere read access to the user’s computer screen. To address the latter vulnerability, we propose a minor modification of the protocol. The threat model we introduce paves the way for the analysis of other CIE MFA protocols.
Pasqua, Michele ; Miculan, Marino: Behavioral equivalences for AbU: Verifying security and safety in distributed IoT systems. In: Theoretical Computer Science vols. 998 (2024), p. 114537
Attribute-based memory Updates (Image 1in short) is an interaction mechanism recently introduced for adapting the Event-Condition-Action (ECA) programming paradigm to distributed reactive systems, such as autonomic and smart IoT device ensembles. In this model, an event (e.g., an input from a sensor, or a device state update) can trigger an ECA rule, whose execution can cause the state update of (possibly) many remote devices at once; the latter are selected “on the fly” by means of predicates over their state, without the need of a central coordinating entity. However, the combination of different Image 1systems may yield unexpected interactions, e.g., when a new device is added to an existing secure system, potentially hindering the security of the whole ensemble of devices. This can be critical in the IoT, where smart devices are more and more pervasive in our daily life. In this paper, we consider the problem of ensuring security and safety requirements for Image 1systems (and, in turn, for IoT devices). The first are a form of noninterference, as they correspond to avoid forbidden information flows (e.g., information flows violating confidentiality); while the second are a form of non-interaction, as they correspond to avoid unintended executions (e.g., leading to erroneous/unsafe states). In order to formally model these requirements, we introduce suitable behavioral equivalences for Image 1. These equivalences are generalizations of hiding bisimilarity, i.e., a kind of weak bisimilarity where we can compare systems up to actions at different levels of security. Leveraging these behavioral equivalences, we propose (syntactic) sufficient conditions guaranteeing the requirements and, then, effective algorithms for statically verifying such conditions.
Castelnovo, Davide ; Gadducci, Fabio ; Miculan, Marino: A simple criterion for 𝓜,𝓝-adhesivity. In: Theoretical Computer Science vols. 982 (2024), p. 114280
Adhesive categories, and variants such as 𝓜,𝓝-adhesive ones, marked a watershed moment for the algebraic approaches to the rewriting of graph-like structures, since they provide an abstract framework where many general results (on e.g. parallelism) could be recast and uniformly proved. However, often checking that a model satisfies the adhesivity properties is far from immediate. In this paper we present a new criterion giving a sufficient condition for 𝓜,𝓝-adhesivity, a generalisation of the original notion of adhesivity. To show the effectiveness of this criterion, we apply it to several existing categories of graph-like structures, including hypergraphs, various kinds of hierarchical graphs (a formalism that is notoriously difficult to fit in the mould of algebraic approaches to rewriting), and combinations of them.
Stolze, Claude ; Miculan, Marino ; Di Gianantonio, Pietro: Composable partial multiparty session types for open systems. In: Software and Systems Modeling, Springer (2023), Nr. 22, pp. 473–494
Voltan, Gabriele ; Foresti, Gian Luca ; Miculan, Marino: Pairing an Autoencoder and a SF-SOINN for Implementing an Intrusion Detection System. In: Proceedings of the Thematic Workshops co-located with the 3rd CINI National Lab AIIS Conference on Artificial Intelligence (Ital-IA 2023), CEUR Workshop Proceedings. vols. 3486 : CEUR-WS.org, 2023, pp. 409–414
Bistarelli, Stefano ; Faloci, Francesco ; Mori, Paolo ; Taticchi, Carlo ; Miculan, Marino: Modeling Carne PRI supply chain with the *-Chain Platform. In: Mori, P. ; Visconti, I. ; Bistarelli, S. (eds.): Proceedings of the Fifth Distributed Ledger Technology Workshop (DLT 2023), Bologna, Italy, May 25-26, 2023, CEUR Workshop Proceedings. vols. 3460 : CEUR-WS.org, 2023
Altarui, Andrea ; Miculan, Marino ; Paier, Matteo: DBCChecker: a Bigraph-based Tool for Checking Security Properties of Container Compositions. In: Buccafurri, F. ; Ferrari, E. ; Lax, G. (eds.): Proceedings of the Italian Conference on Cyber Security (ITASEC 2023), Bari, Italy, May 2-5, 2023, CEUR Workshop Proceedings. vols. 3488 : CEUR-WS.org, 2023
In recent years, event-driven programming languages, in particular those based on Event Condition Action (ECA) rules, have emerged as a promising paradigm for implementing ubiquitous and pervasive systems. These implementations are mostly centralized, where a single server (often in the cloud) collects and processes all the inputs from the environment. In fact, placing the computation on the nodes interacting with the environment requires suitable abstractions for effective communication and coordination of (possibly large) ensembles of these distributed components — abstractions that current ECA languages are still missing. To this end, in this paper we present AbU, a calculus for modeling and reasoning about ECA-based systems with attribute-based communication. The latter is an interaction model recently introduced for the coordination of (possibly large) families of nodes: communication is similar to broadcast but the actual receivers are selected on the spot, by means of predicates over nodes properties. Thus, the programmer can specify interactions between nodes in a declarative way, abstracting from details such as nodes identity, number, or even their existence, without the need for a central server: the computation is moved on the “edge”, thus improving reliability, scalability, privacy and security. After having defined syntax and formal semantics of AbU, we showcase its expressiveness by providing some example applications and the encoding of AbC, the archetypal calculus with attribute-based communication. Then, we focus on two key properties of reactive systems: stabilization (i.e., termination of internal steps) and confluence. For both these properties we provide formal semantic definition, sufficient syntactic conditions on AbU systems, and algorithms to statically check such conditions. Hence, AbU is both a basis for the formal analysis of event-driven architectures with attributed-based interaction, and a reference model for a full-fledged language for IoT and edge computing.
Miculan, Marino ; Vitacolonna, Nicola: Automated Verification of Telegram’s MTProto 2.0 in the Symbolic Model. In: Computers & Security (2023), p. 103072
MTProto 2.0 is the suite of security protocols for instant messaging at the core of the popular Telegram messenger application. In this paper we analyse MTProto 2.0 using ProVerif, a state-of-the-art symbolic security protocol verifier based on the Dolev-Yao model. We provide the first formal symbolic model of MTProto 2.0; in this model, we provide fully automated proofs of the soundness of authentication, normal chat, end-to-end encrypted chat, and rekeying mechanisms with respect to several security properties, including authentication, integrity, secrecy and perfect forward secrecy. At the same time, we discover that the rekeying protocol is vulnerable to an unknown key-share (UKS) attack. To achieve these results, we proceed in an incremental way: each protocol is examined in isolation, relying only on the guarantees provided by the previous ones and the robustness of the basic cryptographic primitives. The importance of this research is threefold. First, it proves the formal correctness of MTProto 2.0 with respect to most relevant security properties. Secondly, we isolate the aspects of cryptographic primitives that escape the symbolic model and thus require further investigation in the computational model. Finally, our modelisation can serve as a reference for the implementation and analysis of clients and servers.
Lab, Cybersecurity: CVE-2023-40718: IPS Engine evasion using custom TCP flags.
Miculan, Marino ; Paier, Matteo: A Calculus for Subjective Communication. In: Dal Lago, U. ; Gorla, D. (eds.): Proceedings of the 23rd Italian Conference on Theoretical Computer Science, ICTCS 2022, Rome, Italy, September 7-9, 2022, CEUR Workshop Proceedings. vols. 3284 : CEUR-WS.org, 2022, pp. 148–160
Pasqua, Michele ; Miculan, Marino: Distributed Programming of Smart Systems with Event-Condition-Action Rules. In: Dal Lago, U. ; Gorla, D. (eds.): Proceedings of the 23rd Italian Conference on Theoretical Computer Science, ICTCS 2022, Rome, Italy, September 7-9, 2022, CEUR Workshop Proceedings. vols. 3284 : CEUR-WS.org, 2022, pp. 201–206
Castelnovo, Davide ; Gadducci, Fabio ; Miculan, Marino: A new criterion for M,N-adhesivity, with an application to hierarchical graphs. In: Proc. FoSSaCS, Lecture Notes in Computer Science. vols. 13242 : Springer, 2022, pp. 205–224
Castelnovo, Davide ; Miculan, Marino: Closure Hyperdoctrines. In: Gadducci, F. ; Silva, A. (eds.): 9th Conference on Algebra and Coalgebra in Computer Science, CALCO 2021, LIPIcs. vols. 211 : Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021, pp. 12:1–12:21
Pasqua, Michele ; Miculan, Marino: On the Security and Safety of AbU Systems. In: Calinescu, R. ; Pasareanu, C. S. (eds.): Software Engineering and Formal Methods (SEFM 2021). vols. 13085 : Springer, 2021 — ISBN 978-3-030-92124-8, pp. 178–198
Attribute-based memory updates (AbU in short) is an interaction mechanism recently introduced for adapting the Event-Condition-Action (ECA) programming paradigm to distributed systems, particularly suited for the IoT. It can be seen as a memory-based counterpart of attribute-based communication, keeping the simplicity of ECA rules.
De Nardin, Axel ; Miculan, Marino ; Piciarelli, Claudio ; Foresti, Gian Luca: A time-series classification approach to shallow web traffic de-anonymization. In: Armando, A. ; Colajanni, M. (eds.): Proceedings of the Fifth Italian Conference on Cyber Security, ITASEC 2021. vols. 2940 : CEUR-WS, 2021, pp. 156–165
Miculan, Marino ; Pasqua, Michele: A Calculus for Attribute-based Memory Updates. In: Cerone, A. ; Ölveczky, P. (eds.): Proceedings of the 18th International Colloquium on Theoretical Aspects of Computing, ICTAC 2021, Lecture Notes in Computer Science. vols. 12819 : Springer, 2021
Miculan, Marino ; Vitacolonna, Nicola: Automated Symbolic Verification of Telegram’s MTProto 2.0. In: Vimercati, S. De Capitani di ; Samarati, P. (eds.): Proceedings of the 18th International Conference on Security and Cryptography, SECRYPT 2021 : SciTePress, 2021. — Best Paper Award — ISBN 978-989-758-524-1, pp. 185–197
Miculan, Marino ; Tosone, Daniel: Securing the Art Market with Distributed Public Ledgers. In: Chiaraluce, F. ; Mostarda, L. (eds.): Proceedings of the 3rd Distributed Ledger Technology Workshop (DLT 2020), CEUR Workshop Proceedings. vols. 2580 : CEUR-WS.org, 2020
Burco, Fabio ; Miculan, Marino ; Peressotti, Marco: Towards a Formal Model for Composable Container Systems. In: Proceedings of the 35th Annual ACM Symposium on Applied Computing (ACM SAC) : ACM, 2020 — ISBN 9781450368667
Miculan, Marino ; Foresti, Gian Luca ; Piciarelli, Claudio: Towards User Recognition by Shallow Web Traffic Inspection. In: Degano, P. ; Zunino, R. (eds.): Proceedings of the Third Italian Conference on Cyber Security, Pisa, Italy, February 13-15, 2019, CEUR Workshop Proceedings. vols. 2315 : CEUR-WS.org, 2019
Geatti, Luca ; Igne, Federico ; Miculan, Marino: An Abstract Distributed Middleware for Transactions over Heterogeneous Stores. In: Cherubini, A. ; Sabadini, N. ; Tini, S. (eds.): Proc. 20th Italian Conference on Theoretical Computer Science, ICTCS 2019, CEUR Workshop Proceedings. vols. 2504 : CEUR-WS.org, 2019, pp. 171–183
We introduce loose graph simulations (LGS), a new notion about labelled graphs which subsumes in an intuitive and natural way subgraph isomorphism (SGI), regular language pattern matching (RLPM) and graph simulation (GS). Being a unification of all these notions, LGS allows us to express directly also problems which are “mixed” instances of previous ones, and hence which would not fit easily in any of them. After the definition and some examples, we show that the problem of finding loose graph simulations is NP-complete, we provide formal translation of SGI, RLPM, and GS into LGSs, and we give the representation of a problem which extends both SGI and RLPM. Finally, we identify a subclass of the LGS problem that is polynomial.
Hildebrandt, T. ; Miculan, M. (eds.): First and Second International Workshops on Meta Models for Process Languages (MeMo), Selected Papers, Journal of Logical and Algebraic Methods in Programming. vols. 95, 2018
Miculan, M. ; Rabe, F. (eds.): LFMTP ’17: Proceedings of the Workshop on Logical Frameworks and Meta-Languages: Theory and Practice : ACM, 2017 — ISBN 978-1-4503-5374-8
Miculan, Marino ; Peressotti, Marco: On the bisimulation hierarchy of state-to-function transition systems. In: Proceedings of ICTCS 2016, CEUR-WS. vols. 1720, 2016, pp. 88–102
Bernardo, Marco ; Miculan, Marino: Disjunctive Probabilistic Modal Logic is Enough for Bisimilarity on Reactive Probabilistic Systems. In: Proceedings of ICTCS 2016, CEUR-WS. vols. 1720, 2016, pp. 203–220
Re, B. ; Miculan, M. (eds.): Special Issue on Methodologies, Technologies and Tools Enabling e-Government, International Journal of Electronic Governance. vols. 8, 2016
Abstract Recently, unifying theories for processes combining non-determinism with quantitative aspects (such as probabilistic or stochastically timed executions) have been proposed with the aim of providing general results and tools. This paper provides two contributions in this respect. First, we present a general {GSOS} specification format and a corresponding notion of bisimulation for non-deterministic processes with quantitative aspects. These specifications define labelled transition systems according to the {ULTraS} model, an extension of the usual {LTSs} where the transition relation associates any source state and transition label with state reachability weight functions (like, e.g., probability distributions). This format, hence called Weight Function {GSOS} (WF-GSOS), covers many known systems and their bisimulations (e.g. PEPA, TIPP, PCSP) and {GSOS} formats (e.g. GSOS, Weighted GSOS, Segala-GSOS). The second contribution is a characterization of these systems as coalgebras of a class of functors, parametric in the weight structure. This result allows us to prove soundness and completeness of the WF-GSOS specification format, and that bisimilarities induced by these specifications are always congruences.
Brengos, Tomasz ; Miculan, Marino ; Peressotti, Marco: Behavioural equivalences for coalgebras with unobservable moves . In: Journal of Logical and Algebraic Methods in Programming vols. 84 (2015), Nr. 6, pp. 826–852
We introduce a general categorical framework for the definition of weak behavioural equivalences, building on and extending recent results in the field. This framework is based on special order enriched categories, i.e. categories whose hom-sets are endowed with suitable complete orders. Using this structure we provide an abstract notion of saturation, which allows us to define various (weak) behavioural equivalences. We show that the Kleisli categories of many common monads are categories of this kind. On one hand, this allows us to instantiate the abstract definitions to a wide range of existing systems (weighted LTS, Segala systems, calculi with names, etc.), recovering the corresponding notions of weak behavioural equivalences; on the other, we can readily provide new weak behavioural equivalences for more complex behaviours, like those definable on presheaves, topological spaces, measurable spaces, etc.
Bacci, Giorgio ; Miculan, Marino: Structural operational semantics for continuous state stochastic transition systems. In: Journal of Computer and System Sciences vols. 81 (2015), pp. 834–858
Abstract In this paper we show how to model syntax and semantics of stochastic processes with continuous states, respectively as algebras and coalgebras of suitable endofunctors over the category of measurable spaces Meas. Moreover, we present an SOS-like rule format, called MGSOS, representing abstract {GSOS} over Meas, and yielding fully abstract universal semantics, for which behavioral equivalence is a congruence. An {MGSOS} specification defines how semantics of processes are composed by means of measure terms, which are expressions specifically designed for describing finite measures. The syntax of these measure terms, and their interpretation as measures, are part of the {MGSOS} specification. We give two example applications, with a simple and neat {MGSOS} specification: a “quantitative CCS”, and a calculus of processes living in the plane R 2 whose communication rate depends on their distance. The approach we follow in these cases can be readily adapted to deal with other quantitative aspects.
Miculan, Marino ; Peressotti, Marco ; Toneguzzo, Andrea: Open Transactions on Shared Memory. In: Holvoet, T. ; Viroli, M. (eds.): Coordination Models and Languages - 17th IFIP WG 6.1 International Conference, COORDINATION 2015, Proceedings, Lecture Notes in Computer Science. vols. 9037 : Springer, 2015, pp. 213–229
Miculan, Marino ; Peressotti, Marco: GSOS for non-deterministic processes with quantitative aspects. In: Bertrand, N. ; Bortolussi, L. (eds.): Proceedings Twelfth International Workshop on Quantitative Aspects of Programming Languages and Systems, QAPL 2014, Grenoble, France, 12-13 April 2014., EPTCS. vols. 154, 2014, pp. 17–33
Bacci, Giorgio ; Miculan, Marino ; Rizzi, Romeo: Finding a Forest in a Tree — The matching problem for wide reactive systems. In: Maffei, M. ; Tuosto, E. (eds.): Trustworthy Global Computing - 9th International Symposium, TGC 2014, Rome, Italy, September 5-6, 2014. Revised Selected Papers, lncs. vols. 8902 : Springer, 2014, pp. 17–33
Bizjak, A. ; Birkedal, Lars ; Miculan, Marino: A Model of Countable Nondeterminism in Guarded Type Theory. In: Dowek, G. (ed.): Proc. RTA-TLCA, lncs. vols. 8560 : Springer, 2014, pp. 108–123
Mansutti, Alessio ; Miculan, Marino ; Peressotti, Marco: Multi-agent Systems Design and Prototyping with Bigraphical Reactive Systems. In: Magoutis, K. ; Pietzuch, P. (eds.): Proc. DAIS 2014, lncs, 2014, pp. 201–208
Re, B. ; Miculan, M. (eds.): Proceedings of the 8th International Conference on Methodologies, Technologies and Tools Enabling e-Government (MeTTeG’14) : Universitas Studiorum, 2014
Miculan, Marino ; Peressotti, Marco: Weak bisimulations for labelled transition systems weighted over semirings. CoRR, abs/1310.4106.
Miculan, Marino ; Paviotti, Marco: Synthesis of Distributed Mobile Programs Using Monadic Types in Coq. In: Beringer, L. ; Felty, A. P. (eds.): Interactive Theorem Proving - Third International Conference, ITP 2012, Princeton, NJ, USA, August 13-15, 2012. Proceedings, Lecture Notes in Computer Science. vols. 7406 : Springer, 2012, pp. 183–200
Miculan, Marino ; Sambarino, Ilaria: Implementing the Stochastics Brane Calculus in a Generic Stochastic Abstract Machine. In: Ciobanu, G. (ed.): Proceedings 6th Workshop on Membrane Computing and Biologically Inspired Process Calculi, Newcastle, UK, 8th September 2012, Electronic Proceedings in Theoretical Computer Science. vols. 100 : Open Publishing Association, 2012, pp. 82–100
Bacci, Giorgio ; Miculan, Marino: Structural operational semantics for continuous state probabilistic processes. In: Proc. CMCS’12, lncs. vols. 7399 : Springer, 2012, pp. 71–90
Miculan, Marino ; Urban, Caterina: Formal analysis of Facebook Connect Single Sign-On authentication protocol. In: SofSem 2011, Proceedings of Student Research Forum : OKAT, 2011. — Best Poster Award, pp. 99–116
Maiero, Carlo ; Miculan, Marino: Unobservable Intrusion Detection Based on Call Traces in Paravirtualized Systems. In: Lopez, J. ; Samarati, P. (eds.): Proc. SECRYPT : SciTePress, 2011
Bacci, Giorgio ; Miculan, Marino: Measurable Stochastics for Brane Calculus. In: Ciobanu, G. ; Koutny, M. (eds.): Proc. MeCBIC, EPTCS. vols. 40, 2010, pp. 6–22
Grohmann, Davide ; Miculan, Marino: Graph Algebras for Bigraphs. In: C. Ermel, J. de L. ; Heckel, R. (eds.): Proc. 9th International Workshop on Graph Transformation and Visual Modeling Techniques (GT-VMT’10), Electronic Communications of the EASST. vols. 10 : European Association of Software Science and Technology, 2010
Crary, Karl ; Miculan, Marino ; Crary, K. ; Miculan, M. (eds.): Proceedings 5th International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, EPTCS. vols. 34, 2010
Bacci, Giorgio ; Grohmann, Davide ; Miculan, Marino: A framework for protein and membrane interactions. In: Ciobanu, G. (ed.): Proc. MeCBIC’09, EPTCS. vols. 11, 2009
Bacci, Giorgio ; Grohmann, Davide ; Miculan, Marino: Bigraphical models for protein and membrane interactions. In: Ciobanu, G. (ed.): Proc. MeCBIC’09, EPTCS. vols. 11, 2009
Grohmann, Davide ; Miculan, Marino: Deriving Barbed Bisimulations for Bigraphical Reactive Systems. In: Corradini, A. ; Tuosto, E. (eds.): Proceedings of International Conference on Graph Transformation (ICGT-DS 2008), Electronic Communications of the EASST. vols. 16 : European Association of Software Science and Technology, 2009
Miculan, M. ; Scagnetto, I. ; Honsell, F. (eds.): Types for Proofs and Programs, International Conference, TYPES 2007, Revised Selected Papers, lncs. vols. 4941 : Springer, 2008 — ISBN 978-3-540-68084-0
Bacci, Giorgio ; Miculan, Marino: Undecidability of Model checking in Brane Logic. In: Proc. 3rd Int. Workshop on Development of Computational Models, DCM’07 vols. 192, Elsevier (2008), Nr. 3
Kahsai, Temesghen ; Miculan, Marino: Implementing Spi-Calculus Using Nominal Techniques. In: Beckmann, A. ; Dimitracopoulos, C. ; Löwe, B. (eds.): Proc. Computability in Europe (CiE), lncs. vols. 5028 : Springer, 2008 — ISBN 978-3-540-69405-2, pp. 294–305
Grohmann, Davide ; Miculan, Marino: An Algebra for Directed Bigraphs. In: Mackie, I. ; Plump, D. (eds.) Proceedings of TERMGRAPH 2007 vols. 203, Elsevier (2008), Nr. 1, pp. 49–63
Grohmann, Davide ; Miculan, Marino: Controlling resource access in Directed Bigraphs (long version). In: C. Ermel, J. de L. ; Heckel, R. (eds.): Proc. 7th International Workshop on Graph Transformation and Visual Modeling Techniques (GT-VMT’08), Electronic Communications of the EASST. vols. 10 : European Association of Software Science and Technology, 2008
Grohmann, Davide ; Miculan, Marino: Reactive Systems over Directed Bigraphs. In: Caires, L. ; Vasconcelos, V. (eds.): Proc. CONCUR 2007, Lecture Notes in Computer Science. vols. 4703 : Springer, 2007 — ISBN 978-3-540-74406-1, pp. 380–394
Ciaffaglione, Alberto ; Liquori, Luigi ; Miculan, Marino: Reasoning about Object-based Calculi in (Co)Inductive Type Theory and the Theory of Contexts. In: J. Autom. Reasoning vols. 39 (2007), Nr. 1, pp. 1–47
Grohmann, Davide ; Miculan, Marino: Directed bigraphs: theory and applications ( Nr. UDMI/12/2006/RR) : Department of Mathematics and Computer Science, University of Udine, 2006
Bucalo, Anna ; Hofmann, Martin ; Honsell, Furio ; Miculan, Marino ; Scagnetto, Ivan: Consistency of the Theory of Contexts. In: Journal of Functional Programming vols. 16 (2006), Nr. 3, pp. 327–395
Gadducci, Fabio ; Miculan, Marino ; Montanari, Ugo: On permutation algebras, (pre)sheaves and named sets. In: Higher-Order and Symbolic Computation vols. 19 (2006), Nr. 2-3, pp. 283–304
Miculan, Marino ; Yemane, Kidane: A Unifying Model of Variables and Names. In: Sassone, V. (ed.): Foundations of Software Science and Computational Structures, 8th International Conference, FOSSACS 2005, Proceedings, Lecture Notes in Computer Science. vols. 3441 : Springer, 2005, pp. 170–186
Honsell, F. ; Lenisa, M. ; Miculan, M. (eds.): Proceedings of the Workshop of the COMETA Project on Computational Metamodels, entcs. vols. 104 : Elsevier, 2004
Di Gianantonio, Pietro ; Miculan, Marino: Unifying Recursive and Co-recursive Definitions in Sheaf Categories. In: Walukiewicz, I. (ed.): Proc. FOSSACS’04, lncs. vols. 2987 : Springer, 2004, pp. 136–150
Ciaffaglione, Alberto ; Liquori, Luigi ; Miculan, Marino: Imperative Object-based Calculi in (Co)Inductive Type Theories. In: Vardi, M. Y. ; Voronkov, A. (eds.): Proc. LPAR, lncs. vols. 2850 : Springer, 2003 — ISBN 3-540-20101-7, pp. 59–77
Di Gianantonio, Pietro ; Miculan, Marino: A Unifying Approach to Recursive and Co-recursive Definitions. In: Geuvers, H. ; Wiedijk, F. (eds.): Proc. TYPES’02, lncs. vols. 2646 : Springer-Verlag, 2003, pp. 148–161
Honsell, F. ; Miculan, M. ; Momigliano, A. (eds.): Proc. 2nd International Workshop on Mechanized Reasoning about Languages with Variable Binding (MERLIN’03), ACM Digital Library : ACM, 2003
Ciaffaglione, Alberto ; Liquori, Luigi ; Miculan, Marino: Reasoning on an Imperative Object-based Calculus in Higher Order Abstract Syntax. In: Honsell, F. ; Miculan, M. ; Momigliano, A. (eds.): Proc. 2nd MERLIN, ACM Digital Library : ACM, 2003
Scagnetto, Ivan ; Miculan, Marino: Ambient Calculus and its Logic in the Calculus of Inductive Constructions. In: Pfenning, F. (ed.): Proc. Third International Workshop on Logical Frameworks and Meta-Languages (LFM’02), entcs. vols. 70.2 : Elsevier, 2002
Burelli, Alessandra ; Miculan, Marino: Frecuencis lessicâls dal furlan scrit. In: Gjornâl furlan des siencis vols. 1 (2002), pp. 167–207
Honsell, Furio ; Miculan, Marino ; Scagnetto, Ivan: An axiomatic approach to metareasoning on systems in higher-order abstract syntax. In: Proc. ICALP’01, lncs. vols. 2076 : Springer-Verlag, 2001, pp. 963–978
Miculan, Marino: Developing (Meta)Theory of Lambda-calculus in the Theory of Contexts. In: Ambler, S. ; Crole, R. ; Momigliano, A. (eds.): Proc. MERLIN 2001, entcs. vols. 58.1 : Elsevier, 2001, pp. 1–22
Miculan, Marino: On the formalization of the modal µ-calculus in the Calculus of Inductive Constructions. In: Information and Computation vols. 164 (2001), Nr. 1, pp. 199–231
Lenisa, M. ; Miculan, M. (eds.): Special Issue about Theory of Concurrency, Higher Order Languages and Types (TOSCA 2001), entcs. vols. 62, 2001
Honsell, Furio ; Miculan, Marino ; Scagnetto, Ivan: The Theory of Contexts for First-Order and Higher-Order Abstract Syntax. In: Proc. TOSCA’01, Electron. Notes Theor. Comput. Sci. vols. 62 : Elsevier, 2001, pp. 111–130
Miculan, Marino: Formalizing a lazy substitution proof system for µ-calculus in the Calculus of Inductive Constructions. In: Proc. ICALP’99, lncs. vols. 1644 : Springer-Verlag, 1999
Cerrato, Simona ; Asnicar, Fabio ; Dall’Aglio, Paolo ; Felice, Amanda de ; Di Fant, Massimo ; Mizzaro, Marco ; Nesti, Fabrizio ; Candusso, Maria ; et al.: The Journal of High Energy Physics: Scientific Publishing on the Web. In: De Bra, P. ; Leggett, J. J. (eds.): Proceedings of WebNet 99 - World Conference on the WWW and Internet, Honolulu, Hawaii, USA, October 24-30, 1999 : AACE, 1999, pp. 1482–1483
Miculan, Marino: A Natural Deduction style proof system for propositional µ-calculus and its formalization in inductive type theories. In: Proc. ICTCS’98 : World Scientific, 1998
Honsell, Furio ; Miculan, Marino: A Natural Deduction Approach to Dynamic Logic. In: Berardi, S. ; Coppo, M. (eds.): Types for Proofs and Programs, International Workshop TYPES’95, Selected Papers, Lecture Notes in Computer Science. vols. 1158 : Springer, 1995, pp. 165–182
Miculan, Marino: The Expressive Power of Structural Operational Semantics with Explicit Assumptions. In: Barendregt, H. ; Nipkow, T. (eds.): Types for Proofs and Programs, International Workshop TYPES’93, Nijmegen, The Netherlands, May 24-28, 1993, Selected Papers, Lecture Notes in Computer Science. vols. 806 : Springer, 1994, pp. 263–290