53 Search Results for "Ferreira, Luís"

Volume

OASIcs, Volume 74

8th Symposium on Languages, Applications and Technologies (SLATE 2019)

SLATE 2019, June 27-28, 2019, Coimbra, Portugal

Editors: Ricardo Rodrigues, Jan Janoušek, Luís Ferreira, Luísa Coheur, Fernando Batista, and Hugo Gonçalo Oliveira

Volume

LIPIcs, Volume 125

22nd International Conference on Principles of Distributed Systems (OPODIS 2018)

OPODIS 2018, December 17-19, 2018, Hong Kong, China

Editors: Jiannong Cao, Faith Ellen, Luis Rodrigues, and Bernardo Ferreira

Document
DOI: 10.4230/LIPIcs.CPM.2026.14
Hardness Results on Characteristics for Elastic-Degenerate Strings

Authors: Dominik Köppl and Jannik Olbrich

Published in: LIPIcs, Volume 369, 37th Annual Symposium on Combinatorial Pattern Matching (CPM 2026)

Abstract
Generalizations of plain strings have been proposed as a compact way to represent a collection of nearly identical sequences or to express uncertainty at specific text positions by enumerating all possibilities. While a plain string stores a character at each of its positions, generalizations consider a set of characters (indeterminate strings), a set of strings of equal length (generalized degenerate strings, or shortly GD strings), or a set of strings of arbitrary lengths (elastic-degenerate strings, or shortly ED strings). These generalizations are of importance to compactly represent such type of data, and find applications in bioinformatics for representing and maintaining a set of genetic sequences of the same taxonomy or a multiple sequence alignment. To be of use, attention has been drawn to answering various query types such as pattern matching or measuring similarity of ED strings by generalizing techniques known to plain strings. However, for some types of queries, it has been shown that a generalization of a polynomial-time solvable query on classic strings becomes NP-hard on ED strings, e.g. [Russo et al., 2022]. In that light, we wonder about other types of queries that are of particular interest to bioinformatics: unique substrings, absent words, anti-powers, longest previous factors, and Lempel-Ziv-like compression schemes. While we obtain a polynomial time algorithm for a variation of longest previous factors, we show that all other problems are NP-hard to compute, some of them even under the restriction that the input can be modeled as an indeterminate or GD string.
Cite as

Dominik Köppl and Jannik Olbrich. Hardness Results on Characteristics for Elastic-Degenerate Strings. In 37th Annual Symposium on Combinatorial Pattern Matching (CPM 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 369, pp. 14:1-14:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{koppl_et_al:LIPIcs.CPM.2026.14,
  author =	{K\"{o}ppl, Dominik and Olbrich, Jannik},
  title =	{{Hardness Results on Characteristics for Elastic-Degenerate Strings}},
  booktitle =	{37th Annual Symposium on Combinatorial Pattern Matching (CPM 2026)},
  pages =	{14:1--14:25},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-420-8},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{369},
  editor =	{Bille, Philip and Prezza, Nicola},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CPM.2026.14},
  URN =		{urn:nbn:de:0030-drops-259409},
  doi =		{10.4230/LIPIcs.CPM.2026.14},
  annote =	{Keywords: Elastic-degenerate strings, NP-hardness, longest common factor, minimal unique substring, minimal absent word, anti-power, longest previous factor}
}
Document
DOI: 10.4230/LIPIcs.DISC.2025.38
Compact Routing Schemes in Undirected and Directed Graphs

Authors: Avi Kadria and Liam Roditty

Published in: LIPIcs, Volume 356, 39th International Symposium on Distributed Computing (DISC 2025)

Abstract
In this paper, we study the problem of compact routing schemes in weighted undirected and directed graphs. For weighted undirected graphs, more than a decade ago, Chechik [PODC'13] presented a ≈ 3.68k-stretch compact routing scheme that uses Õ(n^{1/k}log{D}) local storage, where D is the normalized diameter, for every k > 1. We present a ≈ 2.64k-stretch compact routing scheme that uses Õ(n^{1/k}) local storage on average in each vertex. This is the first compact routing scheme that uses total local storage of Õ(n^{1+1/k}) while achieving a c ⋅ k stretch, for a constant c < 3. In real-world network protocols, messages are usually transmitted as part of a communication session between two parties. Therefore, more than two decades ago, Thorup and Zwick [SPAA'01] considered compact routing schemes that establish a communication session using a handshake. In their handshake-based compact routing scheme, the handshake is routed along a (4k-5)-stretch path, and the rest of the communication session is routed along an optimal (2k-1)-stretch path. It is straightforward to improve the (4k-5)-stretch of the handshake to ≈ 3.68k-stretch using the compact routing scheme of Chechik [PODC'13]. We improve the handshake stretch to the optimal (2k-1), by borrowing the concept of roundtrip routing from directed graphs to undirected graphs. For weighted directed graphs, more than two decades ago, Roditty, Thorup, and Zwick [SODA'02 and TALG'08] presented a (4k+ε)-stretch compact roundtrip routing scheme that uses Õ(n^{1/k}) local storage for every k ≥ 3. For k = 3, this gives a (12+ε)-roundtrip stretch using Õ(n^{1/3}) local storage. We improve the stretch by developing a 7-roundtrip stretch routing scheme with Õ(n^{1/3}) local storage. In addition, we consider graphs with bounded hop diameter and present an optimal (2k-1)-roundtrip stretch routing scheme that uses Õ(D_{HOP}⋅ n^{1/k}), where D_{HOP} is the hop diameter of the graph.
Cite as

Avi Kadria and Liam Roditty. Compact Routing Schemes in Undirected and Directed Graphs. In 39th International Symposium on Distributed Computing (DISC 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 356, pp. 38:1-38:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{kadria_et_al:LIPIcs.DISC.2025.38,
  author =	{Kadria, Avi and Roditty, Liam},
  title =	{{Compact Routing Schemes in Undirected and Directed Graphs}},
  booktitle =	{39th International Symposium on Distributed Computing (DISC 2025)},
  pages =	{38:1--38:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-402-4},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{356},
  editor =	{Kowalski, Dariusz R.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.DISC.2025.38},
  URN =		{urn:nbn:de:0030-drops-248555},
  doi =		{10.4230/LIPIcs.DISC.2025.38},
  annote =	{Keywords: Routing schemes, Compact routing schemes, Distance oracles, Computer networks, Graph algorithms}
}
Document
DOI: 10.4230/LIPIcs.DISC.2025.28
Byzantine Consensus in the Random Asynchronous Model

Authors: George Danezis, Jovan Komatovic, Lefteris Kokoris-Kogias, Alberto Sonnino, and Igor Zablotchi

Published in: LIPIcs, Volume 356, 39th International Symposium on Distributed Computing (DISC 2025)

Abstract
We propose a novel relaxation of the classic asynchronous network model, called the random asynchronous model, which removes adversarial message scheduling while preserving unbounded message delays and Byzantine faults. Instead of an adversary dictating message order, delivery follows a random schedule. We analyze Byzantine consensus at different resilience thresholds (n = 3f+1, n = 2f+1, and n = f+2) and show that our relaxation allows consensus with probabilistic guarantees which are impossible in the standard asynchronous model or even the partially synchronous model. We complement these protocols with corresponding impossibility results, establishing the limits of consensus in the random asynchronous model.
Cite as

George Danezis, Jovan Komatovic, Lefteris Kokoris-Kogias, Alberto Sonnino, and Igor Zablotchi. Byzantine Consensus in the Random Asynchronous Model. In 39th International Symposium on Distributed Computing (DISC 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 356, pp. 28:1-28:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{danezis_et_al:LIPIcs.DISC.2025.28,
  author =	{Danezis, George and Komatovic, Jovan and Kokoris-Kogias, Lefteris and Sonnino, Alberto and Zablotchi, Igor},
  title =	{{Byzantine Consensus in the Random Asynchronous Model}},
  booktitle =	{39th International Symposium on Distributed Computing (DISC 2025)},
  pages =	{28:1--28:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-402-4},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{356},
  editor =	{Kowalski, Dariusz R.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.DISC.2025.28},
  URN =		{urn:nbn:de:0030-drops-248457},
  doi =		{10.4230/LIPIcs.DISC.2025.28},
  annote =	{Keywords: network model, asynchronous, random scheduler, Byzantine consensus}
}
Document
DOI: 10.4230/LIPIcs.AFT.2025.27
Unravelling the Probabilistic Forest: Arbitrage in Prediction Markets

Authors: Oriol Saguillo, Vahid Ghafouri, Lucianna Kiffer, and Guillermo Suarez-Tangil

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

Abstract
Polymarket is a prediction market platform where users can speculate on future events by trading shares tied to specific outcomes, known as conditions. Each market on Polymarket is associated with a set of one or more such conditions. To ensure proper market resolution, the condition set must be exhaustive - collectively accounting for all possible outcomes - and mutually exclusive - only one condition may resolve as true. Thus, the collective prices (probabilities) of all related outcomes (whether in a condition or market) should be $1, representing a combined probability of 1 of any outcome. Despite this design, Polymarket exhibits cases where dependent assets are mispriced, allowing for purchasing (or selling) a certain outcome for less than (or more than) $1, guaranteeing profit. This phenomenon, known as arbitrage, could enable sophisticated participants to exploit such inconsistencies. In this paper, we conduct an empirical arbitrage analysis on Polymarket data to answer three key questions: (Q1) What conditions give rise to arbitrage? (Q2) Does arbitrage actually occur on Polymarket?, and (Q3) Has anyone exploited these opportunities? A major challenge in analyzing arbitrage between related markets lies in the scalability of comparisons across a large number of markets and conditions, with a naive analysis requiring O(2^{n+m}) comparisons. To overcome this, we employ a heuristic-driven reduction strategy based on timeliness, topical similarity, and combinatorial relationships, further validated by expert input. Our study reveals two distinct forms of arbitrage on Polymarket: Market Rebalancing Arbitrage, which occurs within a single market or condition (intra-market), and Combinatorial Arbitrage, which spans across multiple markets (inter-market). We use on-chain historical order book data to analyze when these types of arbitrage opportunities have existed, and when they have been executed by users. We find a realized estimate of 40 million USD of profit extracted across both types of arbitrage during our measurement period.
Cite as

Oriol Saguillo, Vahid Ghafouri, Lucianna Kiffer, and Guillermo Suarez-Tangil. Unravelling the Probabilistic Forest: Arbitrage in Prediction Markets. In 7th Conference on Advances in Financial Technologies (AFT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 354, pp. 27:1-27:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{saguillo_et_al:LIPIcs.AFT.2025.27,
  author =	{Saguillo, Oriol and Ghafouri, Vahid and Kiffer, Lucianna and Suarez-Tangil, Guillermo},
  title =	{{Unravelling the Probabilistic Forest: Arbitrage in Prediction Markets}},
  booktitle =	{7th Conference on Advances in Financial Technologies (AFT 2025)},
  pages =	{27:1--27:24},
  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.27},
  URN =		{urn:nbn:de:0030-drops-247468},
  doi =		{10.4230/LIPIcs.AFT.2025.27},
  annote =	{Keywords: Prediction Markets, Maximal Extractable Value, Large Language Models}
}
Document
DOI: 10.4230/LIPIcs.ITP.2025.15
Certified Implementability of Global Multiparty Protocols

Authors: Elaine Li and Thomas Wies

Published in: LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025)

Abstract
Implementability is the decision problem at the heart of top-down approaches to protocol verification. In this paper, we present a mechanization of a recently proposed precise implementability characterization by Li et al. for a large class of protocols that subsumes many existing formalisms in the literature. Our protocols and implementations model asynchronous commmunication, and can exhibit infinite behavior. We improve upon their pen-and-paper results by unifying distinct formalisms, simplifying existing proof arguments, elaborating on the construction of canonical implementations, and even uncovering a subtle bug in the semantics for infinite words. As a corollary of our mechanization, we show that the original characterization of implementability applies even to protocols with infinitely many participants. We also contribute a reusable library for reasoning about generic communicating state machines. Our mechanization consists of about 15k lines of Rocq code. We believe that our mechanization can provide the foundation for deductively proving the implementability of protocols beyond the reach of prior work, extracting certified implementations for finite protocols, and investigating implementability under alternative asynchronous communication models.
Cite as

Elaine Li and Thomas Wies. Certified Implementability of Global Multiparty Protocols. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 15:1-15:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{li_et_al:LIPIcs.ITP.2025.15,
  author =	{Li, Elaine and Wies, Thomas},
  title =	{{Certified Implementability of Global Multiparty Protocols}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{15:1--15:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-396-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{352},
  editor =	{Forster, Yannick and Keller, Chantal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.15},
  URN =		{urn:nbn:de:0030-drops-246139},
  doi =		{10.4230/LIPIcs.ITP.2025.15},
  annote =	{Keywords: Asynchronous protocols, communicating state machines, labeled transition systems, infinite semantics, realizability, multiparty session types, choreographies, deadlock freedom}
}
Document
DOI: 10.4230/OASIcs.Programming.2025.9
COP Layer Encapsulating Non-Functional Requirements for Physical Systems on Hakoniwa Environment

Authors: Yudai Yamada, Nobuhiko Ogura, Kenji Hisazumi, and Harumi Watanabe

Published in: OASIcs, Volume 134, Companion Proceedings of the 9th International Conference on the Art, Science, and Engineering of Programming (Programming 2025)

Abstract
This paper contributes to solving two issues: (1) clearly defining Non-Functional Requirements (NFRs) and Functional Requirements (FRs), and (2) simulating on a practical IoT platform. Related to the first problem, we always feel annoyed with many irregular conditions and non-requirements for programming physical systems. Particularly, they sometimes cause cross-cutting concerns problems. Thus, we cannot concentrate on mainstream behavior. Regarding the second problem, the platform must deal with IoT problems. Modern physical systems are integrated with the Internet of Things (IoT), which connects multiple devices, sensors, and cloud services. As a result, these systems may face problems such as latency, race conditions, deadlocks, and more. To solve these problems, we propose a robot software development environment called CPy4NFR. For the first problem, we draw NFRs in feature models, and CPy4NFR generates layers of Context-Oriented Programming (COP). The programming language is called CPy, which is an extension of Python. Through this process, the relation between non-functional requirements and COP is clarified, and the cross-cutting concern problems are solved. Regarding the second problem, CPy programs with NFRs are executed on Hakoniwa. Hakoniwa deals with IoT problems, provides APIs for simulator environments such as Unity and Unreal Engine, and supports APIs for physical robot systems. In this paper, we apply CPy4NFR to develop a drone system with changing behavior at runtime. Finally, we discuss two problems and the proposed development environment.
Cite as

Yudai Yamada, Nobuhiko Ogura, Kenji Hisazumi, and Harumi Watanabe. COP Layer Encapsulating Non-Functional Requirements for Physical Systems on Hakoniwa Environment. In Companion Proceedings of the 9th International Conference on the Art, Science, and Engineering of Programming (Programming 2025). Open Access Series in Informatics (OASIcs), Volume 134, pp. 9:1-9:10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{yamada_et_al:OASIcs.Programming.2025.9,
  author =	{Yamada, Yudai and Ogura, Nobuhiko and Hisazumi, Kenji and Watanabe, Harumi},
  title =	{{COP Layer Encapsulating Non-Functional Requirements for Physical Systems on Hakoniwa Environment}},
  booktitle =	{Companion Proceedings of the 9th International Conference on the Art, Science, and Engineering of Programming (Programming 2025)},
  pages =	{9:1--9:10},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-382-9},
  ISSN =	{2190-6807},
  year =	{2025},
  volume =	{134},
  editor =	{Edwards, Jonathan and Perera, Roly and Petricek, Tomas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.Programming.2025.9},
  URN =		{urn:nbn:de:0030-drops-242931},
  doi =		{10.4230/OASIcs.Programming.2025.9},
  annote =	{Keywords: Context-Oriented Programming, Non-Functional Requirement, Real-Time System}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2024.6
Data Types with Symmetries via Action Containers

Authors: Philipp Joram and Niccolò Veltri

Published in: LIPIcs, Volume 336, 30th International Conference on Types for Proofs and Programs (TYPES 2024)

Abstract
We study two kinds of containers for data types with symmetries in homotopy type theory, and clarify their relationship by introducing the intermediate notion of action containers. Quotient containers are set-valued containers with groups of permissible permutations of positions, interpreted as (possibly non-finitary) analytic functors on the category of sets. Symmetric containers encode symmetries in a groupoid of shapes, and are interpreted accordingly as polynomial functors on the 2-category of groupoids. Action containers are endowed with groups that act on their positions, with morphisms preserving the actions. We show that, as a category, action containers are equivalent to the free coproduct completion of a category of group actions. We derive that they model non-inductive single-variable strictly positive types in the sense of Abbott et al.: The category of action containers is closed under arbitrary (co)products and exponentiation with constants. We equip this category with the structure of a locally groupoidal 2-category, and prove that it locally embeds into the 2-category of symmetric containers. This follows from the embedding of a 2-category of groups into the 2-category of groupoids, extending the delooping construction.
Cite as

Philipp Joram and Niccolò Veltri. Data Types with Symmetries via Action Containers. In 30th International Conference on Types for Proofs and Programs (TYPES 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 336, pp. 6:1-6:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{joram_et_al:LIPIcs.TYPES.2024.6,
  author =	{Joram, Philipp and Veltri, Niccol\`{o}},
  title =	{{Data Types with Symmetries via Action Containers}},
  booktitle =	{30th International Conference on Types for Proofs and Programs (TYPES 2024)},
  pages =	{6:1--6:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-376-8},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{336},
  editor =	{M{\o}gelberg, Rasmus Ejlers and van den Berg, Benno},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2024.6},
  URN =		{urn:nbn:de:0030-drops-233681},
  doi =		{10.4230/LIPIcs.TYPES.2024.6},
  annote =	{Keywords: Containers, Homotopy Type Theory, Agda, 2-categories}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2025.10
Bottom-Up Synthesis of Memory Mutations with Separation Logic

Authors: Kasra Ferdowsi and Hila Peleg

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

Abstract
Programming-by-Example (PBE) is the paradigm of program synthesis specified via input-output pairs. It is commonly used because examples are easy to provide and collect from the environment. A popular optimization for enumerative synthesis with examples is Observational Equivalence (OE), which groups programs into equivalence classes according to their evaluation on example inputs. Current formulations of OE, however, are severely limited by the assumption that the synthesizer’s target language contains only pure components with no side-effects, either enforcing this in their target language, or ignoring it, leading to an incorrect enumeration. This limits their ability to use realistic component sets. We address this limitation by borrowing from Separation Logic, which can compositionally reason about heap mutations. We reformulate PBE using a restricted Separation Logic: Concrete Heap Separation Logic (CHSL), transforming the search for programs into a proof search in CHSL. This lets us perform bottom-up enumerative synthesis without the need for expert-provided annotations or domain-specific inferences, but with three key advantages: we (i) preserve correctness in the presence of memory-mutating operations, (ii) compact the search space by representing many concrete programs as one under CHSL, and (iii) perform a provably correct OE-reduction. We present SObEq (Side-effects in OBservational EQuivalence), a bottom-up enumerative algorithm that, given a PBE task, searches for its CHSL derivation. The SObEq algorithm is proved correct with no purity assumptions: we show it is guaranteed to lose no solutions. We also evaluate our implementation of SObEq on benchmarks from the literature and online sources, and show that it produces high-quality results quickly.
Cite as

Kasra Ferdowsi and Hila Peleg. Bottom-Up Synthesis of Memory Mutations with Separation Logic. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 10:1-10:32, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{ferdowsi_et_al:LIPIcs.ECOOP.2025.10,
  author =	{Ferdowsi, Kasra and Peleg, Hila},
  title =	{{Bottom-Up Synthesis of Memory Mutations with Separation Logic}},
  booktitle =	{39th European Conference on Object-Oriented Programming (ECOOP 2025)},
  pages =	{10:1--10:32},
  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.10},
  URN =		{urn:nbn:de:0030-drops-233036},
  doi =		{10.4230/LIPIcs.ECOOP.2025.10},
  annote =	{Keywords: Program synthesis, observational equivalence}
}
Document
DOI: 10.4230/LIPIcs.OPODIS.2024.8
Optimal Multilevel Slashing for Blockchains

Authors: Kenan Wood, Hammurabi Mendes, and Jonad Pulaj

Published in: LIPIcs, Volume 324, 28th International Conference on Principles of Distributed Systems (OPODIS 2024)

Abstract
We present the notion of multilevel slashing, where proof-of-stake blockchain validators can obtain gradual levels of assurance that a certain block is bound to be finalized in a global consensus procedure, unless an increasing and optimally large number of Byzantine processes have their staked assets slashed - that is, deducted - due to provably incorrect behavior. Our construction is a highly parameterized generalization of combinatorial intersection systems based on finite projective spaces, with asymptotic high availability and optimal slashing properties. Even under weak conditions, we show that our construction has asymptotically optimal slashing properties with respect to message complexity and validator load; this result also illustrates a fundamental trade off between message complexity, load, and slashing. In addition, we show that any intersection system whose ground elements are disjoint subsets of nodes (e.g. "committees" in committee-based consensus protocols) has asymptotic high availability under similarly weak conditions. Finally, our multilevel construction gives the flexibility to blockchain validators to decide how many "levels" of finalization assurance they wish to obtain. This functionality can be seen either as (i) a form of an early, slashing-based block finalization; or (ii) a service to support reorg tolerance.
Cite as

Kenan Wood, Hammurabi Mendes, and Jonad Pulaj. Optimal Multilevel Slashing for Blockchains. In 28th International Conference on Principles of Distributed Systems (OPODIS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 324, pp. 8:1-8:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{wood_et_al:LIPIcs.OPODIS.2024.8,
  author =	{Wood, Kenan and Mendes, Hammurabi and Pulaj, Jonad},
  title =	{{Optimal Multilevel Slashing for Blockchains}},
  booktitle =	{28th International Conference on Principles of Distributed Systems (OPODIS 2024)},
  pages =	{8:1--8:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-360-7},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{324},
  editor =	{Bonomi, Silvia and Galletta, Letterio and Rivi\`{e}re, Etienne and Schiavoni, Valerio},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.OPODIS.2024.8},
  URN =		{urn:nbn:de:0030-drops-225445},
  doi =		{10.4230/LIPIcs.OPODIS.2024.8},
  annote =	{Keywords: Blockchains, Finality, Slashablility, Committees, Availability}
}
Document
DOI: 10.4230/LITES.8.2.2
Swarms of Mobile Robots: Towards Versatility with Safety

Authors: Pierre Courtieu, Lionel Rieg, Sébastien Tixeuil, and Xavier Urbain

Published in: LITES, Volume 8, Issue 2 (2022): Special Issue on Distributed Hybrid Systems. Leibniz Transactions on Embedded Systems, Volume 8, Issue 2

Abstract
We present Pactole, a formal framework to design and prove the correctness of protocols (or the impossibility of their existence) that target mobile robotic swarms. Unlike previous approaches, our methodology unifies in a single formalism the execution model, the problem specification, the protocol, and its proof of correctness. The Pactole framework makes use of the Coq proof assistant, and is specially targeted at protocol designers and problem specifiers, so that a common unambiguous language is used from the very early stages of protocol development. We stress the underlying framework design principles to enable high expressivity and modularity, and provide concrete examples about how the Pactole framework can be used to tackle actual problems, some previously addressed by the Distributed Computing community, but also new problems, while being certified correct.
Cite as

Pierre Courtieu, Lionel Rieg, Sébastien Tixeuil, and Xavier Urbain. Swarms of Mobile Robots: Towards Versatility with Safety. In LITES, Volume 8, Issue 2 (2022): Special Issue on Distributed Hybrid Systems. Leibniz Transactions on Embedded Systems, Volume 8, Issue 2, pp. 02:1-02:36, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@Article{courtieu_et_al:LITES.8.2.2,
  author =	{Courtieu, Pierre and Rieg, Lionel and Tixeuil, S\'{e}bastien and Urbain, Xavier},
  title =	{{Swarms of Mobile Robots: Towards Versatility with Safety}},
  journal =	{Leibniz Transactions on Embedded Systems},
  pages =	{02:1--02:36},
  ISSN =	{2199-2002},
  year =	{2022},
  volume =	{8},
  number =	{2},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LITES.8.2.2},
  URN =		{urn:nbn:de:0030-drops-192942},
  doi =		{10.4230/LITES.8.2.2},
  annote =	{Keywords: distributed algorithm, mobile autonomous robots, formal proof}
}
Document
DOI: 10.4230/OASIcs.SLATE.2022.3
Question Answering For Toxicological Information Extraction

Authors: Bruno Carlos Luís Ferreira, Hugo Gonçalo Oliveira, Hugo Amaro, Ângela Laranjeiro, and Catarina Silva

Published in: OASIcs, Volume 104, 11th Symposium on Languages, Applications and Technologies (SLATE 2022)

Abstract
Working with large amounts of text data has become hectic and time-consuming. In order to reduce human effort, costs, and make the process more efficient, companies and organizations resort to intelligent algorithms to automate and assist the manual work. This problem is also present in the field of toxicological analysis of chemical substances, where information needs to be searched from multiple documents. That said, we propose an approach that relies on Question Answering for acquiring information from unstructured data, in our case, English PDF documents containing information about physicochemical and toxicological properties of chemical substances. Experimental results confirm that our approach achieves promising results which can be applicable in the business scenario, especially if further revised by humans.
Cite as

Bruno Carlos Luís Ferreira, Hugo Gonçalo Oliveira, Hugo Amaro, Ângela Laranjeiro, and Catarina Silva. Question Answering For Toxicological Information Extraction. In 11th Symposium on Languages, Applications and Technologies (SLATE 2022). Open Access Series in Informatics (OASIcs), Volume 104, pp. 3:1-3:10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{ferreira_et_al:OASIcs.SLATE.2022.3,
  author =	{Ferreira, Bruno Carlos Lu{\'\i}s and Gon\c{c}alo Oliveira, Hugo and Amaro, Hugo and Laranjeiro, \^{A}ngela and Silva, Catarina},
  title =	{{Question Answering For Toxicological Information Extraction}},
  booktitle =	{11th Symposium on Languages, Applications and Technologies (SLATE 2022)},
  pages =	{3:1--3:10},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-245-7},
  ISSN =	{2190-6807},
  year =	{2022},
  volume =	{104},
  editor =	{Cordeiro, Jo\~{a}o and Pereira, Maria Jo\~{a}o and Rodrigues, Nuno F. and Pais, Sebasti\~{a}o},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.SLATE.2022.3},
  URN =		{urn:nbn:de:0030-drops-167493},
  doi =		{10.4230/OASIcs.SLATE.2022.3},
  annote =	{Keywords: Information Extraction, Question Answering, Transformers, Toxicological Analysis}
}
Document
DOI: 10.4230/LITES.7.1.1
Randomization as Mitigation of Directed Timing Inference Based Attacks on Time-Triggered Real-Time Systems with Task Replication

Authors: Kristin Krüger, Nils Vreman, Richard Pates, Martina Maggio, Marcus Völp, and Gerhard Fohler

Published in: LITES, Volume 7, Issue 1 (2021): Special Issue on Embedded System Security. Leibniz Transactions on Embedded Systems, Volume 7, Issue 1

Abstract
Time-triggered real-time systems achieve deterministic behavior using schedules that are constructed offline, based on scheduling constraints. Their deterministic behavior makes time-triggered systems suitable for usage in safety-critical environments, like avionics. However, this determinism also allows attackers to fine-tune attacks that can be carried out after studying the behavior of the system through side channels, targeting safety-critical victim tasks. Replication -- i.e., the execution of task variants across different cores -- is inherently able to tolerate both accidental and malicious faults (i.e. attacks) as long as these faults are independent of one another. Yet, targeted attacks on the timing behavior of tasks which utilize information gained about the system behavior violate the fault independence assumption fault tolerance is based on. This violation may give attackers the opportunity to compromise all replicas simultaneously, in particular if they can mount the attack from already compromised components. In this paper, we analyze vulnerabilities of time-triggered systems, focusing on safety-certified multicore real-time systems. We introduce two runtime mitigation strategies to withstand directed timing inference based attacks: (i) schedule randomization at slot level, and (ii) randomization within a set of offline constructed schedules. We evaluate these mitigation strategies with synthetic experiments and a real case study to show their effectiveness and practicality.
Cite as

Kristin Krüger, Nils Vreman, Richard Pates, Martina Maggio, Marcus Völp, and Gerhard Fohler. Randomization as Mitigation of Directed Timing Inference Based Attacks on Time-Triggered Real-Time Systems with Task Replication. In LITES, Volume 7, Issue 1 (2021): Special Issue on Embedded System Security. Leibniz Transactions on Embedded Systems, Volume 7, Issue 1, pp. 01:1-01:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@Article{kruger_et_al:LITES.7.1.1,
  author =	{Kr\"{u}ger, Kristin and Vreman, Nils and Pates, Richard and Maggio, Martina and V\"{o}lp, Marcus and Fohler, Gerhard},
  title =	{{Randomization as Mitigation of Directed Timing Inference Based Attacks on Time-Triggered Real-Time Systems with Task Replication}},
  journal =	{Leibniz Transactions on Embedded Systems},
  pages =	{01:1--01:29},
  ISSN =	{2199-2002},
  year =	{2021},
  volume =	{7},
  number =	{1},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LITES.7.1.1},
  URN =		{urn:nbn:de:0030-drops-192847},
  doi =		{10.4230/LITES.7.1.1},
  annote =	{Keywords: real-time systems, time-triggered systems, security}
}
Document
DOI: 10.4230/OASIcs.ICPEC.2020.6
An Augmented Reality Mathematics Serious Game

Authors: José Manuel Cerqueira, João Martinho Moura, Cristina Sylla, and Luís Ferreira

Published in: OASIcs, Volume 81, First International Computer Programming Education Conference (ICPEC 2020)

Abstract
This article presents the results obtained from an experiment using an Augmented Reality (AR) serious game for learning mathematical functions in middle school, in contexts that resort to Game Based Learning. A serious game was created specifically for this purpose and allowed to conduct an exploratory study with a quantitative and qualitative methodological approach, with two groups of teachers of different subjects: mathematics and informatics. The game, called FootMath, allows the visualization, manipulation and exploration of linear, quadratic, exponential and trigonometric mathematical functions, through the simulation of a 3D football game, in which the user can change the function parameters with different values, in order to score a goal. It was tested the potential use of AR technologies in learning scenarios, considering the teacher’s perspective. According to the findings, FootMath was considered to be a promising and innovative tool to be incorporated in real mathematics teaching scenarios.
Cite as

José Manuel Cerqueira, João Martinho Moura, Cristina Sylla, and Luís Ferreira. An Augmented Reality Mathematics Serious Game. In First International Computer Programming Education Conference (ICPEC 2020). Open Access Series in Informatics (OASIcs), Volume 81, pp. 6:1-6:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{cerqueira_et_al:OASIcs.ICPEC.2020.6,
  author =	{Cerqueira, Jos\'{e} Manuel and Moura, Jo\~{a}o Martinho and Sylla, Cristina and Ferreira, Lu{\'\i}s},
  title =	{{An Augmented Reality Mathematics Serious Game}},
  booktitle =	{First International Computer Programming Education Conference (ICPEC 2020)},
  pages =	{6:1--6:8},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-153-5},
  ISSN =	{2190-6807},
  year =	{2020},
  volume =	{81},
  editor =	{Queir\'{o}s, Ricardo and Portela, Filipe and Pinto, M\'{a}rio and Sim\~{o}es, Alberto},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.ICPEC.2020.6},
  URN =		{urn:nbn:de:0030-drops-122939},
  doi =		{10.4230/OASIcs.ICPEC.2020.6},
  annote =	{Keywords: Serious Game, Augmented Reality, Mathematics, Functions}
}
  • Refine by Type
  • 51 Document/PDF
  • 9 Document/HTML
  • 2 Volume

  • Refine by Publication Year
  • 1 2026
  • 8 2025
  • 2 2022
  • 1 2021
  • 2 2020
  • Show More...

  • Refine by Author
  • 4 Ferreira, Luís
  • 3 Gonçalo Oliveira, Hugo
  • 2 Batista, Fernando
  • 2 Cao, Jiannong
  • 2 Censor-Hillel, Keren
  • Show More...

  • Refine by Series/Journal
  • 41 LIPIcs
  • 7 OASIcs
  • 3 LITES

  • Refine by Classification
  • 13 Theory of computation → Distributed algorithms
  • 7 Theory of computation → Distributed computing models
  • 3 Theory of computation → Self-organization
  • 2 Computer systems organization → Dependable and fault-tolerant systems and networks
  • 2 Computer systems organization → Real-time systems
  • Show More...

  • Refine by Keyword
  • 3 Blockchain
  • 3 consensus
  • 2 Augmented Reality
  • 2 Conference Organization
  • 2 Consensus
  • 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