9 Search Results for "Murgia, Maurizio"

Document
Artifact
DOI: 10.4230/DARTS.12.1.22
Automatic Code and Test Generation of Smart Contracts from Coordination Models (Artifact)

Authors: Elvis Konjoh Selabi, Maurizio Murgia, António Ravara, and Emilio Tuosto

Published in: DARTS, Volume 12, Issue 1, Special Issue of the 40th European Conference on Object-Oriented Programming (ECOOP 2026)

Abstract
The companion paper proposes a formal approach for specifying and implementing decentralised coordination in distributed systems, with a focus on smart contracts. The model captures dynamic roles, data-driven transitions, and external coordination interfaces, enabling high-level reasoning about decentralised workflows. A toolchain supports formal model validation, Solidity code generation (extensible to other smart contract languages), and automated test synthesis. Although targeting blockchain platforms, the methodology is platform-agnostic and may generalise to other service-oriented and distributed architectures. The expressiveness and practicality of the approach are demonstrated through modelling and realising coordination patterns in smart contracts. This artifact accompanies our paper [Elvis Konjoh Selabi et al., 2026]. It provides a toolchain for generating smart contract code from EDAM (Extended Data-Aware Machines) specifications. The artifact includes the complete source code, a Docker image for easy deployment, pre-generated experiment data (generated code, automated tests, and mutation testing results), and reproduction scripts.
Cite as

Elvis Konjoh Selabi, Maurizio Murgia, António Ravara, and Emilio Tuosto. Automatic Code and Test Generation of Smart Contracts from Coordination Models (Artifact). In Special Issue of the 40th European Conference on Object-Oriented Programming (ECOOP 2026). Dagstuhl Artifacts Series (DARTS), Volume 12, Issue 1, pp. 22:1-22:9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@Article{konjohselabi_et_al:DARTS.12.1.22,
  author =	{Konjoh Selabi, Elvis and Murgia, Maurizio and Ravara, Ant\'{o}nio and Tuosto, Emilio},
  title =	{{Automatic Code and Test Generation of Smart Contracts from Coordination Models (Artifact)}},
  pages =	{22:1--22:9},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2026},
  volume =	{12},
  number =	{1},
  editor =	{Konjoh Selabi, Elvis and Murgia, Maurizio and Ravara, Ant\'{o}nio and Tuosto, Emilio},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.12.1.22},
  URN =		{urn:nbn:de:0030-drops-261590},
  doi =		{10.4230/DARTS.12.1.22},
  annote =	{Keywords: Smart Contracts, Coordination Models, Formal Semantics, Role-Based Access, Decentralised Systems, Code Generation, Solidity, Verification}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2026.15
Automatic Code and Test Generation of Smart Contracts from Coordination Models

Authors: Elvis Konjoh Selabi, Maurizio Murgia, António Ravara, and Emilio Tuosto

Published in: LIPIcs, Volume 372, 40th European Conference on Object-Oriented Programming (ECOOP 2026)

Abstract
We propose a formal approach for specifying and implementing decentralised coordination in distributed systems, with a focus on smart contracts. Our model captures dynamic roles, data-driven transitions, and external coordination interfaces, enabling high-level reasoning about decentralised workflows. We implement a toolchain that supports formal model validation, code generation for Solidity (our framework is extendable to other smart contract languages), and automated test synthesis. Although our implementation targets blockchain platforms, the methodology is platform-agnostic and may generalise to other service-oriented and distributed architectures. We demonstrate the expressiveness and practicality of the approach by modelling and realising some coordination patterns in smart contracts.
Cite as

Elvis Konjoh Selabi, Maurizio Murgia, António Ravara, and Emilio Tuosto. Automatic Code and Test Generation of Smart Contracts from Coordination Models. In 40th European Conference on Object-Oriented Programming (ECOOP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 372, pp. 15:1-15:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{konjohselabi_et_al:LIPIcs.ECOOP.2026.15,
  author =	{Konjoh Selabi, Elvis and Murgia, Maurizio and Ravara, Ant\'{o}nio and Tuosto, Emilio},
  title =	{{Automatic Code and Test Generation of Smart Contracts from Coordination Models}},
  booktitle =	{40th European Conference on Object-Oriented Programming (ECOOP 2026)},
  pages =	{15:1--15:30},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-423-9},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{372},
  editor =	{Krebbers, Robbert and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2026.15},
  URN =		{urn:nbn:de:0030-drops-261119},
  doi =		{10.4230/LIPIcs.ECOOP.2026.15},
  annote =	{Keywords: Smart Contracts, Coordination Models, Formal Semantics, Role-Based Access, Decentralised Systems, Code Generation, Solidity, Verification}
}
Document
DOI: 10.4230/LIPIcs.SEA.2026.23
Exploiting Multi-Core Parallelism in Blockchain Validation and Construction

Authors: Arivarasan Karmegam, Lucianna Kiffer, and Antonio Fernández Anta

Published in: LIPIcs, Volume 371, 24th International Symposium on Experimental Algorithms (SEA 2026)

Abstract
Blockchain validators can reduce block processing time by exploiting multi-core CPUs, but deterministic execution must preserve a given total order while respecting transaction conflicts and per-block runtime limits. This paper systematically examines how validators can exploit multi-core parallelism during both block construction and execution without violating blockchain semantics. We formalize two validator-side optimization problems: (i) executing an already ordered block on p cores to minimize makespan while ensuring equivalence to sequential execution; and (ii) selecting and scheduling a subset of mempool transactions under a runtime limit B to maximize validator reward. For both, we develop exact Mixed-Integer Linear Programming (MILP) formulations that capture conflict, order, and capacity constraints, and propose fast deterministic heuristics that scale to realistic workloads. Using Ethereum mainnet traces and including a Solana-inspired declared-access baseline (Sol) for ordered-block scheduling and a simple reward-greedy baseline (RG) for block construction, we empirically quantify the trade-offs between optimality and runtime. MILPs quickly become intractable as heterogeneity or core count increases, whereas our heuristics run in milliseconds and achieve near-optimal quality. For ordered-block execution, heuristic makespans are typically within a few percent of the MILP solutions (and can even surpass the MILP incumbent when the solver times out), yielding up to 1.5 speedup with p = 2 and 2.3 speedup with p = 8 over sequential execution, despite tight ordering constraints. For block construction, the heuristic achieves 99-100% of the MILP optimum reward on homogeneous workloads, and 74-100% of an LP-relaxation upper bound on heterogeneous workloads, where exact optimization often times out. The resulting block-construction throughput scales close to linearly with p, reaching up to 7.9 speedup with p = 8 in our experiments. These results demonstrate that lightweight, conflict-aware scheduling and selection can unlock substantial parallelism in blockchain validation, bridging the gap between sequential execution and the true potential of multi-core hardware.
Cite as

Arivarasan Karmegam, Lucianna Kiffer, and Antonio Fernández Anta. Exploiting Multi-Core Parallelism in Blockchain Validation and Construction. In 24th International Symposium on Experimental Algorithms (SEA 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 371, pp. 23:1-23:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{karmegam_et_al:LIPIcs.SEA.2026.23,
  author =	{Karmegam, Arivarasan and Kiffer, Lucianna and Fern\'{a}ndez Anta, Antonio},
  title =	{{Exploiting Multi-Core Parallelism in Blockchain Validation and Construction}},
  booktitle =	{24th International Symposium on Experimental Algorithms (SEA 2026)},
  pages =	{23:1--23:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-422-2},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{371},
  editor =	{Aum\"{u}ller, Martin and Finocchi, Irene},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SEA.2026.23},
  URN =		{urn:nbn:de:0030-drops-260271},
  doi =		{10.4230/LIPIcs.SEA.2026.23},
  annote =	{Keywords: Block construction, Block execution, Deterministic parallelism, Conflict-aware scheduling}
}
Document
DOI: 10.4230/LIPIcs.AFT.2025.23
Transaction Fee Market Design for Parallel Execution

Authors: Bahar Acilan, Andrei Constantinescu, Lioba Heimbach, and Roger Wattenhofer

Published in: LIPIcs, Volume 354, 7th Conference on Advances in Financial Technologies (AFT 2025)

Abstract
Given the low throughput of blockchains like Bitcoin and Ethereum, scalability - the ability to process an increasing number of transactions - has become a central focus of blockchain research. One promising approach is the parallelization of transaction execution across multiple threads. However, achieving efficient parallelization requires a redesign of the incentive structure within the fee market. Currently, the fee market does not differentiate between transactions that access multiple high-demand storage keys (i.e., unique identifiers for individual data entries) versus a single low-demand one, as long as they require the same computational effort. Addressing this discrepancy is crucial for enabling more effective parallel execution. In this work, we aim to bridge the gap between the current fee market and the need for parallel execution by exploring alternative fee market designs. To this end, we propose a framework consisting of two key components: a Gas Computation Mechanism (GCM), which quantifies the load a transaction places on the network in terms of parallelization and computation, measured in units of gas, and a Transaction Fee Mechanism (TFM), which assigns a price to each unit of gas. We additionally introduce a set of desirable properties for a GCM, propose several candidate mechanisms, and evaluate them against these criteria. Our analysis highlights two strong candidates: the weighted area GCM, which integrates smoothly with existing TFMs such as EIP‑1559 and satisfies a broad subset of the outlined properties, and the time-proportional makespan GCM, which assigns gas costs based on the context of the entire block’s schedule and, through this dependence on the overall execution outcome, captures the dynamics of parallel execution more accurately.
Cite as

Bahar Acilan, Andrei Constantinescu, Lioba Heimbach, and Roger Wattenhofer. Transaction Fee Market Design for Parallel Execution. In 7th Conference on Advances in Financial Technologies (AFT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 354, pp. 23:1-23:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{acilan_et_al:LIPIcs.AFT.2025.23,
  author =	{Acilan, Bahar and Constantinescu, Andrei and Heimbach, Lioba and Wattenhofer, Roger},
  title =	{{Transaction Fee Market Design for Parallel Execution}},
  booktitle =	{7th Conference on Advances in Financial Technologies (AFT 2025)},
  pages =	{23:1--23:25},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-400-0},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{354},
  editor =	{Avarikioti, Zeta and Christin, Nicolas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.AFT.2025.23},
  URN =		{urn:nbn:de:0030-drops-247426},
  doi =		{10.4230/LIPIcs.AFT.2025.23},
  annote =	{Keywords: blockchain, transaction fee mechanism, parallel execution}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2025.10
Abstract Subtyping for Asynchronous Multiparty Sessions

Authors: Laura Bocchi, Andy King, Maurizio Murgia, and Simon Thompson

Published in: LIPIcs, Volume 348, 36th International Conference on Concurrency Theory (CONCUR 2025)

Abstract
Session subtyping answers the question of whether a program in a communicating system can be safely substituted for another, when their communication behaviour is described by session types. Asynchronous session subtyping is undecidable, even for two participants, hence the interest in sound, but incomplete, subtyping algorithms. Asynchronous multiparty subtyping can be formulated by decomposing session types into single input and output types which preclude, respectively, external and internal choice. This paper shows how abstract interpretation can sit atop this approach and how it leads to an algorithm that can prove subtyping for intricate communication patterns.
Cite as

Laura Bocchi, Andy King, Maurizio Murgia, and Simon Thompson. Abstract Subtyping for Asynchronous Multiparty Sessions. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 10:1-10:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{bocchi_et_al:LIPIcs.CONCUR.2025.10,
  author =	{Bocchi, Laura and King, Andy and Murgia, Maurizio and Thompson, Simon},
  title =	{{Abstract Subtyping for Asynchronous Multiparty Sessions}},
  booktitle =	{36th International Conference on Concurrency Theory (CONCUR 2025)},
  pages =	{10:1--10:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-389-8},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{348},
  editor =	{Bouyer, Patricia and van de Pol, Jaco},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.10},
  URN =		{urn:nbn:de:0030-drops-239605},
  doi =		{10.4230/LIPIcs.CONCUR.2025.10},
  annote =	{Keywords: asynchrony, session subtyping, automata, abstract interpretation}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2025.11
A Sound and Complete Characterization of Fair Asynchronous Session Subtyping

Authors: Mario Bravetti, Luca Padovani, and Gianluigi Zavattaro

Published in: LIPIcs, Volume 348, 36th International Conference on Concurrency Theory (CONCUR 2025)

Abstract
Session types are abstractions of communication protocols enabling the static analysis of message-passing processes. Refinement notions for session types are key to support safe forms of process substitution while preserving their compatibility with the rest of the system. Recently, a fair refinement relation for asynchronous session types has been defined allowing the anticipation of message outputs with respect to an unbounded number of message inputs. This refinement is useful to capture common patterns in communication protocols that take advantage of asynchrony. However, while the semantic (à la testing) definition of such refinement is straightforward, its characterization has proved to be quite challenging. In fact, only a sound but not complete characterization is known so far. In this paper we close this open problem by presenting a sound and complete characterization of asynchronous fair refinement for session types. We relate this characterization to those given in the literature for synchronous session types by leveraging a novel labelled transition system of session types that embeds their asynchronous semantics.
Cite as

Mario Bravetti, Luca Padovani, and Gianluigi Zavattaro. A Sound and Complete Characterization of Fair Asynchronous Session Subtyping. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 11:1-11:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{bravetti_et_al:LIPIcs.CONCUR.2025.11,
  author =	{Bravetti, Mario and Padovani, Luca and Zavattaro, Gianluigi},
  title =	{{A Sound and Complete Characterization of Fair Asynchronous Session Subtyping}},
  booktitle =	{36th International Conference on Concurrency Theory (CONCUR 2025)},
  pages =	{11:1--11:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-389-8},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{348},
  editor =	{Bouyer, Patricia and van de Pol, Jaco},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.11},
  URN =		{urn:nbn:de:0030-drops-239615},
  doi =		{10.4230/LIPIcs.CONCUR.2025.11},
  annote =	{Keywords: Binary sessions, session types, fair asynchronous subtyping}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2025.24
Fair Termination of Asynchronous Binary Sessions

Authors: Luca Padovani and Gianluigi Zavattaro

Published in: LIPIcs, Volume 333, 39th European Conference on Object-Oriented Programming (ECOOP 2025)

Abstract
We study a theory of asynchronous session types ensuring that well-typed processes terminate under a suitable fairness assumption. Fair termination entails starvation freedom and orphan message freedom namely that all messages, including those that are produced early taking advantage of asynchrony, are eventually consumed. The theory is based on a novel fair asynchronous subtyping relation for session types that is coarser than the existing ones. The type system is also the first of its kind that is firmly rooted in linear logic: fair asynchronous subtyping is incorporated as a natural generalization of the cut and axiom rules of linear logic and asynchronous communication is modeled through a suitable set of commuting conversions and of deep cut reductions in linear logic proofs.
Cite as

Luca Padovani and Gianluigi Zavattaro. Fair Termination of Asynchronous Binary Sessions. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 24:1-24:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{padovani_et_al:LIPIcs.ECOOP.2025.24,
  author =	{Padovani, Luca and Zavattaro, Gianluigi},
  title =	{{Fair Termination of Asynchronous Binary Sessions}},
  booktitle =	{39th European Conference on Object-Oriented Programming (ECOOP 2025)},
  pages =	{24:1--24:29},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-373-7},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{333},
  editor =	{Aldrich, Jonathan and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2025.24},
  URN =		{urn:nbn:de:0030-drops-233169},
  doi =		{10.4230/LIPIcs.ECOOP.2025.24},
  annote =	{Keywords: Binary sessions, fair asynchronous subtyping, fair termination, linear logic}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2023.38
Contextual Behavioural Metrics

Authors: Ugo Dal Lago and Maurizio Murgia

Published in: LIPIcs, Volume 279, 34th International Conference on Concurrency Theory (CONCUR 2023)

Abstract
We introduce contextual behavioural metrics (CBMs) as a novel way of measuring the discrepancy in behaviour between processes, taking into account both quantitative aspects and contextual information. This way, process distances by construction take the environment into account: two (non-equivalent) processes may still exhibit very similar behaviour in some contexts, e.g., when certain actions are never performed. We first show how CBMs capture many well-known notions of equivalence and metric, including Larsen’s environmental parametrized bisimulation. We then study compositional properties of CBMs with respect to some common process algebraic operators, namely prefixing, restriction, non-deterministic sum, parallel composition and replication.
Cite as

Ugo Dal Lago and Maurizio Murgia. Contextual Behavioural Metrics. In 34th International Conference on Concurrency Theory (CONCUR 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 279, pp. 38:1-38:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{dallago_et_al:LIPIcs.CONCUR.2023.38,
  author =	{Dal Lago, Ugo and Murgia, Maurizio},
  title =	{{Contextual Behavioural Metrics}},
  booktitle =	{34th International Conference on Concurrency Theory (CONCUR 2023)},
  pages =	{38:1--38:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-299-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{279},
  editor =	{P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.38},
  URN =		{urn:nbn:de:0030-drops-190320},
  doi =		{10.4230/LIPIcs.CONCUR.2023.38},
  annote =	{Keywords: Behavioural metrics, Labelled Transition Systems, Differential Semantics}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2018.40
Progress-Preserving Refinements of CTA

Authors: Massimo Bartoletti, Laura Bocchi, and Maurizio Murgia

Published in: LIPIcs, Volume 118, 29th International Conference on Concurrency Theory (CONCUR 2018)

Abstract
We develop a theory of refinement for timed asynchronous systems, in the setting of Communicating Timed Automata (CTA). Our refinement applies point-wise to the components of a system of CTA, and only affecting their time constraints - in this way, we achieve compositionality and decidability. We then establish a decidable condition under which our refinement preserves behavioural properties of systems, such as their global and local progress. Our theory provides guidelines on how to implement timed protocols using the real-time primitives of programming languages. We validate our theory through a series of experiments, supported by an open-source tool which implements our verification techniques.
Cite as

Massimo Bartoletti, Laura Bocchi, and Maurizio Murgia. Progress-Preserving Refinements of CTA. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 40:1-40:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{bartoletti_et_al:LIPIcs.CONCUR.2018.40,
  author =	{Bartoletti, Massimo and Bocchi, Laura and Murgia, Maurizio},
  title =	{{Progress-Preserving Refinements of CTA}},
  booktitle =	{29th International Conference on Concurrency Theory (CONCUR 2018)},
  pages =	{40:1--40:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-087-3},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{118},
  editor =	{Schewe, Sven and Zhang, Lijun},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.40},
  URN =		{urn:nbn:de:0030-drops-95786},
  doi =		{10.4230/LIPIcs.CONCUR.2018.40},
  annote =	{Keywords: protocol implementation, communicating timed automata, message passing}
}
  • Refine by Type
  • 9 Document/PDF
  • 5 Document/HTML

  • Refine by Publication Year
  • 3 2026
  • 4 2025
  • 1 2023
  • 1 2018

  • Refine by Author
  • 5 Murgia, Maurizio
  • 2 Bocchi, Laura
  • 2 Konjoh Selabi, Elvis
  • 2 Padovani, Luca
  • 2 Ravara, António
  • Show More...

  • Refine by Series/Journal
  • 8 LIPIcs
  • 1 DARTS

  • Refine by Classification
  • 2 Software and its engineering → Domain specific languages
  • 2 Software and its engineering → Formal methods
  • 2 Theory of computation → Process calculi
  • 2 Theory of computation → Program reasoning
  • 2 Theory of computation → Program semantics
  • Show More...

  • Refine by Keyword
  • 2 Binary sessions
  • 2 Code Generation
  • 2 Coordination Models
  • 2 Decentralised Systems
  • 2 Formal Semantics
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact