10 Search Results for "Ravara, António"

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/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}
}
Artifact
Software
DOI: 10.4230/artifacts.25682
Hypothesis2Daml

Authors: Miguel Valido

Abstract
Cite as

Miguel Valido. Hypothesis2Daml (Software, Source Code). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@misc{dagstuhl-artifact-25682,
   title = {{Hypothesis2Daml}}, 
   author = {Valido, Miguel},
   note = {Software, swhId: \href{https://archive.softwareheritage.org/swh:1:dir:42946bbde2f05418d3a606258a87246557211531;origin=https://github.com/miguelvalido02/Hypothesis2Daml;visit=swh:1:snp:8ffad8aa2b471541dc1c896902692724de652514;anchor=swh:1:rev:3743d1f5e0b4a11c53d00ffa24ea6b6f5ecc320a}{\texttt{swh:1:dir:42946bbde2f05418d3a606258a87246557211531}} (visited on 2026-05-20)},
   url = {https://github.com/miguelvalido02/Hypothesis2Daml},
   doi = {10.4230/artifacts.25682},
}
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.ECOOP.2025.32
Compositional Static Value Analysis for Higher-Order Numerical Programs

Authors: Milla Valnet, Raphaël Monat, and Antoine Miné

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

Abstract
Static analyzers have been successfully developed to detect runtime errors in many languages. However, the automatic analysis of functional languages remains a challenge due to their recursive functions, recursive algebraic data types, and higher-order functions. Classic type systems provide compositional methods that are in general not precise enough to prove the absence of runtime errors such as assertion failures. At the other end of the spectrum, deductive methods are more expressive but may require user guidance to prove invariants. Our work describes a static value analysis by abstract interpretation for a higher-order pure functional language. This analysis provides a sound and automatic approach to discover invariants and prevent assertion and match failures. We have designed a compositional analysis: functions are analyzed only once, at their definition site, generating a summary of their behavior. The summaries can be viewed as input-output relations expressed with relational abstract domains. We present two new abstract domains. A first abstract domain summarizes recursive algebraic data types. A second abstract domain lifts existing disjunctive relational summaries to higher-order by formalizing them as domains able to abstract higher-order functions. Both abstractions are parameterized by the abstractions of basic types (strings, integers, ...). Thanks to this parametric nature, both domains can be combined, allowing the analysis of higher-order functions manipulating algebraic data types and, conversely, algebraic data types using functions as first-class values. We have implemented this analysis in the open-source MOPSA platform. Preliminary evaluation confirms the precision of our approach on a set of 40 handwritten toy programs as well as 20 programs from the state-of-the-art Salto analyzer benchmark.
Cite as

Milla Valnet, Raphaël Monat, and Antoine Miné. Compositional Static Value Analysis for Higher-Order Numerical Programs. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 32:1-32:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{valnet_et_al:LIPIcs.ECOOP.2025.32,
  author =	{Valnet, Milla and Monat, Rapha\"{e}l and Min\'{e}, Antoine},
  title =	{{Compositional Static Value Analysis for Higher-Order Numerical Programs}},
  booktitle =	{39th European Conference on Object-Oriented Programming (ECOOP 2025)},
  pages =	{32:1--32: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.32},
  URN =		{urn:nbn:de:0030-drops-233249},
  doi =		{10.4230/LIPIcs.ECOOP.2025.32},
  annote =	{Keywords: Static Value Analysis, Functional Programming, Abstract Interpretation}
}
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
DOI: 10.4230/LIPIcs.ECOOP.2024.17
Fair Join Pattern Matching for Actors

Authors: Philipp Haller, Ayman Hussein, Hernán Melgratti, Alceste Scalas, and Emilio Tuosto

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

Abstract
Join patterns provide a promising approach to the development of concurrent and distributed message-passing applications. Several variations and implementations have been presented in the literature - but various aspects remain under-explored: in particular, how to specify a suitable notion of message matching, how to implement it correctly and efficiently, and how to systematically evaluate the implementation performance. In this work we focus on actor-based programming, and study the application of join patterns with conditional guards (i.e., the most expressive and challenging version of join patterns in literature). We formalise a novel specification of fair and deterministic join pattern matching, ensuring that older messages are always consumed if they can be matched. We present a stateful, tree-based join pattern matching algorithm and prove that it correctly implements our fair and deterministic matching specification. We present a novel Scala 3 actor library (called JoinActors) that implements our join pattern formalisation, leveraging macros to provide an intuitive API. Finally, we evaluate the performance of our implementation, by introducing a systematic benchmarking approach that takes into account the nuances of join pattern matching (in particular, its sensitivity to input traffic and complexity of patterns and guards).
Cite as

Philipp Haller, Ayman Hussein, Hernán Melgratti, Alceste Scalas, and Emilio Tuosto. Fair Join Pattern Matching for Actors. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 17:1-17:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{haller_et_al:LIPIcs.ECOOP.2024.17,
  author =	{Haller, Philipp and Hussein, Ayman and Melgratti, Hern\'{a}n and Scalas, Alceste and Tuosto, Emilio},
  title =	{{Fair Join Pattern Matching for Actors}},
  booktitle =	{38th European Conference on Object-Oriented Programming (ECOOP 2024)},
  pages =	{17:1--17: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.17},
  URN =		{urn:nbn:de:0030-drops-208663},
  doi =		{10.4230/LIPIcs.ECOOP.2024.17},
  annote =	{Keywords: Concurrency, join patterns, join calculus, actor model}
}
Document
Artifact
DOI: 10.4230/DARTS.10.2.8
Fair Join Pattern Matching for Actors (Artifact)

Authors: Philipp Haller, Ayman Hussein, Hernán Melgratti, Alceste Scalas, and Emilio Tuosto

Published in: DARTS, Volume 10, Issue 2, Special Issue of the 38th European Conference on Object-Oriented Programming (ECOOP 2024)

Abstract
Join patterns provide a promising approach to the development of concurrent and distributed message-passing applications. Several variations and implementations have been presented in the literature - but various aspects remain under-explored: in particular, how to specify a suitable notion of message matching, how to implement it correctly and efficiently, and how to systematically evaluate the implementation performance. In this work we focus on actor-based programming, and study the application of join patterns with conditional guards (i.e., the most expressive and challenging version of join patterns in literature). We formalise a novel specification of fair and deterministic join pattern matching, ensuring that older messages are always consumed if they can be matched. We present a stateful, tree-based join pattern matching algorithm and prove that it correctly implements our fair and deterministic matching specification. We present a novel Scala 3 actor library (called JoinActors) that implements our join pattern formalisation, leveraging macros to provide an intuitive API. Finally, we evaluate the performance of our implementation, by introducing a systematic benchmarking approach that takes into account the nuances of join pattern matching (in particular, its sensitivity to input traffic and complexity of patterns and guards).
Cite as

Philipp Haller, Ayman Hussein, Hernán Melgratti, Alceste Scalas, and Emilio Tuosto. Fair Join Pattern Matching for Actors (Artifact). In Special Issue of the 38th European Conference on Object-Oriented Programming (ECOOP 2024). Dagstuhl Artifacts Series (DARTS), Volume 10, Issue 2, pp. 8:1-8:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@Article{haller_et_al:DARTS.10.2.8,
  author =	{Haller, Philipp and Hussein, Ayman and Melgratti, Hern\'{a}n and Scalas, Alceste and Tuosto, Emilio},
  title =	{{Fair Join Pattern Matching for Actors (Artifact)}},
  pages =	{8:1--8:3},
  journal =	{Dagstuhl Artifacts Series},
  ISBN =	{978-3-95977-342-3},
  ISSN =	{2509-8195},
  year =	{2024},
  volume =	{10},
  number =	{2},
  editor =	{Haller, Philipp and Hussein, Ayman and Melgratti, Hern\'{a}n and Scalas, Alceste 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.10.2.8},
  URN =		{urn:nbn:de:0030-drops-209062},
  doi =		{10.4230/DARTS.10.2.8},
  annote =	{Keywords: Concurrency, join patterns, join calculus, actor model}
}
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}
}
  • Refine by Type
  • 9 Document/PDF
  • 3 Document/HTML
  • 1 Artifact

  • Refine by Publication Year
  • 4 2026
  • 2 2025
  • 3 2024
  • 1 2023

  • Refine by Author
  • 5 Ravara, António
  • 4 Tuosto, Emilio
  • 2 Giunti, Marco
  • 2 Haller, Philipp
  • 2 Hussein, Ayman
  • Show More...

  • Refine by Series/Journal
  • 6 LIPIcs
  • 1 OASIcs
  • 2 DARTS

  • Refine by Classification
  • 4 Software and its engineering → Domain specific languages
  • 2 Software and its engineering → Concurrent programming languages
  • 2 Software and its engineering → Distributed programming languages
  • 2 Software and its engineering → Formal language definitions
  • 2 Software and its engineering → Formal methods
  • Show More...

  • Refine by Keyword
  • 2 Blockchain
  • 2 Code Generation
  • 2 Concurrency
  • 2 Coordination Models
  • 2 Daml
  • 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