Search Results

Documents authored by Ravara, António

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
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/OASIcs.FMBC.2026.5
Smart Tests for a Smart Contract Language

Authors: Miguel Valido and António Ravara

Published in: OASIcs, Volume 142, 7th International Workshop on Formal Methods for Blockchains (FMBC 2026)

Abstract
Smart contracts are high-stakes software: their immutable, publicly accessible, code may govern assets worth millions, meaning that even minor defects can have severe consequences. The most used techniques to ensure smart contract correctness are testing and formal verification. Testing is almost always employed but is often restricted to unit tests (which often miss edge cases) and has limited coverage, while formal verification can provide strong guarantees but is often costly and complex to apply, demanding substantial time and expertise. Property-based testing bridges this gap by exploring large input spaces and shrinking failures to minimal counterexamples, helping uncover defects early in development. Formal verification can be left to critical features once testing has filtered out common issues. To add to the challenges smart contract developers face, most languages used were not designed with safety and security guarantees built-in. Daml is a smart contract language designed with correctness in mind, featuring a strong static type system, functional programming paradigms, and built-in abstractions for common smart contract patterns. However, Daml currently lacks support for property-based testing, limiting developers' ability to systematically explore input spaces and verify contract properties. This paper introduces Hypothesis2Daml, an open-source library that brings property-based testing to the Daml ecosystem by connecting the Hypothesis testing framework with the Daml JSON API. Hypothesis2Daml enables developers to specify invariants, preconditions, and stateful workflows over realistic ledger interactions, while providing automatic input generation, shrinking, and isolation of ledger state between test cases. The approach is evaluated using a benchmark consisting of eight contracts, three Daml templates, and twenty-eight property-based tests covering happy paths, negative cases, and alternative interaction orders. The results show that property-based testing is feasible for Daml smart contracts, can systematically expose violated properties with minimal counterexamples, and supports effective debugging of realistic, stateful workflows.
Cite as

Miguel Valido and António Ravara. Smart Tests for a Smart Contract Language. In 7th International Workshop on Formal Methods for Blockchains (FMBC 2026). Open Access Series in Informatics (OASIcs), Volume 142, pp. 5:1-5:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{valido_et_al:OASIcs.FMBC.2026.5,
  author =	{Valido, Miguel and Ravara, Ant\'{o}nio},
  title =	{{Smart Tests for a Smart Contract Language}},
  booktitle =	{7th International Workshop on Formal Methods for Blockchains (FMBC 2026)},
  pages =	{5:1--5:14},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-424-6},
  ISSN =	{2190-6807},
  year =	{2026},
  volume =	{142},
  editor =	{Bartoletti, Massimo and Marmsoler, Diego},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2026.5},
  URN =		{urn:nbn:de:0030-drops-257021},
  doi =		{10.4230/OASIcs.FMBC.2026.5},
  annote =	{Keywords: Smart contracts, Blockchain, Daml, Property-based testing, Hypothesis}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2024.5
Behavioural Up/down Casting For Statically Typed Languages

Authors: Lorenzo Bacchiani, Mario Bravetti, Marco Giunti, João Mota, and António Ravara

Published in: LIPIcs, Volume 313, 38th European Conference on Object-Oriented Programming (ECOOP 2024)

Abstract
We provide support for polymorphism in static typestate analysis for object-oriented languages with upcasts and downcasts. Recent work has shown how typestate analysis can be embedded in the development of Java programs to obtain safer behaviour at runtime, e.g., absence of null pointer errors and protocol completion. In that approach, inheritance is supported at the price of limiting casts in source code, thus only allowing those at the beginning of the protocol, i.e., immediately after objects creation, or at the end, and in turn seriously affecting the applicability of the analysis. In this paper, we provide a solution to this open problem in typestate analysis by introducing a theory based on a richer data structure, named typestate tree, which supports upcast and downcast operations at any point of the protocol by leveraging union and intersection types. The soundness of the typestate tree-based approach has been mechanised in Coq. The theory can be applied to most object-oriented languages statically analysable through typestates, thus opening new scenarios for acceptance of programs exploiting inheritance and casting. To defend this thesis, we show an application of the theory, by embedding the typestate tree mechanism in a Java-like object-oriented language, and proving its soundness.
Cite as

Lorenzo Bacchiani, Mario Bravetti, Marco Giunti, João Mota, and António Ravara. Behavioural Up/down Casting For Statically Typed Languages. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 5:1-5:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{bacchiani_et_al:LIPIcs.ECOOP.2024.5,
  author =	{Bacchiani, Lorenzo and Bravetti, Mario and Giunti, Marco and Mota, Jo\~{a}o and Ravara, Ant\'{o}nio},
  title =	{{Behavioural Up/down Casting For Statically Typed Languages}},
  booktitle =	{38th European Conference on Object-Oriented Programming (ECOOP 2024)},
  pages =	{5:1--5:28},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-341-6},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{313},
  editor =	{Aldrich, Jonathan and Salvaneschi, Guido},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2024.5},
  URN =		{urn:nbn:de:0030-drops-208543},
  doi =		{10.4230/LIPIcs.ECOOP.2024.5},
  annote =	{Keywords: Behavioural types, object-oriented programming, subtyping, cast, typestates}
}
Document
Experience Paper
DOI: 10.4230/LIPIcs.ECOOP.2023.40
On Using VeriFast, VerCors, Plural, and KeY to Check Object Usage (Experience Paper)

Authors: João Mota, Marco Giunti, and António Ravara

Published in: LIPIcs, Volume 263, 37th European Conference on Object-Oriented Programming (ECOOP 2023)

Abstract
Typestates are a notion of behavioral types that describe protocols for stateful objects, specifying the available methods for each state. Ensuring methods are called in the correct order (protocol compliance), and that, if and when the program terminates, all objects are in the final state (protocol completion) is crucial to write better and safer programs. Objects of this kind are commonly shared among different clients or stored in collections, which may also be shared. However, statically checking protocol compliance and completion when objects are shared is challenging. To evaluate the support given by state of the art verification tools in checking the correct use of shared objects with protocol, we present a survey on four tools for Java: VeriFast, VerCors, Plural, and KeY. We describe the implementation of a file reader, linked-list, and iterator, check for each tool its ability to statically guarantee protocol compliance and completion, even when objects are shared in collections, and evaluate the programmer’s effort in making the code acceptable to these tools. With this study, we motivate the need for lightweight methods to verify the presented kinds of programs.
Cite as

João Mota, Marco Giunti, and António Ravara. On Using VeriFast, VerCors, Plural, and KeY to Check Object Usage (Experience Paper). In 37th European Conference on Object-Oriented Programming (ECOOP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 263, pp. 40:1-40:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{mota_et_al:LIPIcs.ECOOP.2023.40,
  author =	{Mota, Jo\~{a}o and Giunti, Marco and Ravara, Ant\'{o}nio},
  title =	{{On Using VeriFast, VerCors, Plural, and KeY to Check Object Usage}},
  booktitle =	{37th European Conference on Object-Oriented Programming (ECOOP 2023)},
  pages =	{40:1--40:29},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-281-5},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{263},
  editor =	{Ali, Karim and Salvaneschi, Guido},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2023.40},
  URN =		{urn:nbn:de:0030-drops-182330},
  doi =		{10.4230/LIPIcs.ECOOP.2023.40},
  annote =	{Keywords: Java, Typestates, VeriFast, VerCors, Plural, KeY}
}
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