21 Search Results for "Ferreira, João F."

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/OASIcs.AEiC.2026.2
Discovering and Repairing Flaws in C Binaries Without Requiring Codebase and Instrumentation

Authors: Diogo Ferreira and Ibéria Medeiros

Published in: OASIcs, Volume 143, 30th Ada-Europe International Conference on Reliable Software Technologies (AEiC 2026)

Abstract
Industrial and embedded software systems frequently integrate various third-party components sourced from diverse providers into their codebases. These systems are commonly developed in C, a language known for its lack of variable bounds checking, making it vulnerable to Buffer Overflows (BOs), which, when exploited, can cause severe damage. Consequently, the binary code resulting from vulnerable C programs is also vulnerable and remains so in the final products. Fixing these software systems is challenging because only binary code is available. This paper presents PatchBin, a binary patching tool to automatically fix BO vulnerabilities and validate the effectiveness of fixes while ensuring no new flaws are introduced. The approach involves a combination of fuzzing, reverse static analysis and static rewriting techniques to, respectively, (i) identify possible malicious inputs that can trigger BOs, (ii) find their root cause by employing reverse data flow analysis, and (iii) remove them by rewriting the binary code with effective validation, thus generating a new binary without the original flaws and new ones. Experimental evaluations with synthetic and real-world applications demonstrated that PatchBin detects and fixes BO in binary programs without introducing new vulnerabilities. The results showed that PatchBin is an important aid for industrial partners, enabling them to test and fix their products, including third-party components, without access to source code, but only to binary code.
Cite as

Diogo Ferreira and Ibéria Medeiros. Discovering and Repairing Flaws in C Binaries Without Requiring Codebase and Instrumentation. In 30th Ada-Europe International Conference on Reliable Software Technologies (AEiC 2026). Open Access Series in Informatics (OASIcs), Volume 143, pp. 2:1-2:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{ferreira_et_al:OASIcs.AEiC.2026.2,
  author =	{Ferreira, Diogo and Medeiros, Ib\'{e}ria},
  title =	{{Discovering and Repairing Flaws in C Binaries Without Requiring Codebase and Instrumentation}},
  booktitle =	{30th Ada-Europe International Conference on Reliable Software Technologies (AEiC 2026)},
  pages =	{2:1--2:19},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-425-3},
  ISSN =	{2190-6807},
  year =	{2026},
  volume =	{143},
  editor =	{Filieri, Antonio and Backeman, Peter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.AEiC.2026.2},
  URN =		{urn:nbn:de:0030-drops-259209},
  doi =		{10.4230/OASIcs.AEiC.2026.2},
  annote =	{Keywords: Buffer Overflow Vulnerabilities, Binary Patching, Reverse Engineering, Static Analysis, Software Security}
}
Document
Research
DOI: 10.4230/OASIcs.Grossi.14
Specific Patterns Against Reference Sequences

Authors: Marie-Pierre Béal and Maxime Crochemore

Published in: OASIcs, Volume 132, From Strings to Graphs, and Back Again: A Festschrift for Roberto Grossi's 60th Birthday (2025)

Abstract
We design alignment-free techniques for comparing a set of sequences or just a word, called a target, against another set of words, called a reference. This is done with the detection of factor patterns that distinguish the target from the reference. A target-specific factor of a target T against a reference R is then a factor w of a word in T that is not a factor of a word in R but whose proper factors of w are factors of a word in R. The strategy is based on the notion of minimal absent/forbidden words. We first address the computation of the set of target-specific factors of a target T against a reference R, where T and R are finite sets of sequences. The result is the construction of an automaton accepting the set of all considered target-specific factors. The construction algorithm runs in linear time according to the size of T ∪ R. The second result is the design of an algorithm to compute all the occurrences in a single sequence T of its target-specific factors against a reference R. The algorithm runs in real-time on the target sequence, independently of the number of occurrences of target-specific factors.
Cite as

Marie-Pierre Béal and Maxime Crochemore. Specific Patterns Against Reference Sequences. In From Strings to Graphs, and Back Again: A Festschrift for Roberto Grossi's 60th Birthday. Open Access Series in Informatics (OASIcs), Volume 132, pp. 14:1-14:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{beal_et_al:OASIcs.Grossi.14,
  author =	{B\'{e}al, Marie-Pierre and Crochemore, Maxime},
  title =	{{Specific Patterns Against Reference Sequences}},
  booktitle =	{From Strings to Graphs, and Back Again: A Festschrift for Roberto Grossi's 60th Birthday},
  pages =	{14:1--14:12},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-391-1},
  ISSN =	{2190-6807},
  year =	{2025},
  volume =	{132},
  editor =	{Conte, Alessio and Marino, Andrea and Rosone, Giovanna and Vitter, Jeffrey Scott},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.Grossi.14},
  URN =		{urn:nbn:de:0030-drops-238130},
  doi =		{10.4230/OASIcs.Grossi.14},
  annote =	{Keywords: Specific pattern, Minimal absent word, Minimal forbidden word, Directed Acyclic Word Graph (DAWG), Suffix automaton}
}
Document
DOI: 10.4230/OASIcs.SLATE.2025.10
Stepwise Source, a Supporting Tool for Source Code Demonstration

Authors: João Santos, Alvaro Costa Neto, and Pedro Rangel Henriques

Published in: OASIcs, Volume 135, 14th Symposium on Languages, Applications and Technologies (SLATE 2025)

Abstract
The difficulties in teaching and learning computer programming remain a pressing issue to this day. Several studies and tools have been developed over the years to tackle this challenge from many different points-of-view. One of the biggest tools an educator has to support him in a classroom is the progressive explanation of how a source code is constructed and what effects each of its parts has on the overall result. Attempts to translate this live-directed tool to an on-line experience is usually time-consuming and lacking in features. In order to tackle this concern, a tool to create piecewise source code writing demonstrations was developed - Stepwise Source. The main idea behind this application is to allow step-by-step explanation of a source code construction, along with any relevant annotations and automatically assessed challenges that an educator may add. By providing a dynamic platform for both students and lecturers, this software aims to improve the teaching and learning of computer programming, while trying to imitate the information flow of a live lecture, with the added benefit of student-directed pace of explanation. Through interactive guidance and automated assessment, this tool has the potential to foster a deeper understanding of computational principles and promote proficiency in programming skills.
Cite as

João Santos, Alvaro Costa Neto, and Pedro Rangel Henriques. Stepwise Source, a Supporting Tool for Source Code Demonstration. In 14th Symposium on Languages, Applications and Technologies (SLATE 2025). Open Access Series in Informatics (OASIcs), Volume 135, pp. 10:1-10:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{santos_et_al:OASIcs.SLATE.2025.10,
  author =	{Santos, Jo\~{a}o and Costa Neto, Alvaro and Henriques, Pedro Rangel},
  title =	{{Stepwise Source, a Supporting Tool for Source Code Demonstration}},
  booktitle =	{14th Symposium on Languages, Applications and Technologies (SLATE 2025)},
  pages =	{10:1--10:15},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-387-4},
  ISSN =	{2190-6807},
  year =	{2025},
  volume =	{135},
  editor =	{Baptista, Jorge and Barateiro, Jos\'{e}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.SLATE.2025.10},
  URN =		{urn:nbn:de:0030-drops-236906},
  doi =		{10.4230/OASIcs.SLATE.2025.10},
  annote =	{Keywords: Computer Programming Education, Source Code Demonstration, Education Technology}
}
Document
Track A: Algorithms, Complexity and Games
DOI: 10.4230/LIPIcs.ICALP.2025.60
Random Reed-Solomon Codes Achieve the Half-Singleton Bound for Insertions and Deletions over Linear-Sized Alphabets

Authors: Roni Con, Zeyu Guo, Ray Li, and Zihan Zhang

Published in: LIPIcs, Volume 334, 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025)

Abstract
In this paper, we prove that with high probability, random Reed-Solomon codes approach the half-Singleton bound - the optimal rate versus error tradeoff for linear insdel codes - with linear-sized alphabets. More precisely, we prove that, for any ε > 0 and positive integers n and k, with high probability, random Reed-Solomon codes of length n and dimension k can correct (1-ε)n-2k+1 adversarial insdel errors over alphabets of size n+2^{poly(1/ε)}k. This significantly improves upon the alphabet size demonstrated in the work of Con, Shpilka, and Tamo (IEEE TIT, 2023), who showed the existence of Reed-Solomon codes with exponential alphabet size Õ(binom(n,2k-1)²) precisely achieving the half-Singleton bound. Our methods are inspired by recent works on list-decoding Reed-Solomon codes. Brakensiek-Gopi-Makam (STOC 2023) showed that random Reed-Solomon codes are list-decodable up to capacity with exponential-sized alphabets, and Guo-Zhang (FOCS 2023) and Alrabiah-Guruswami-Li (STOC 2024) improved the alphabet-size to linear. We achieve a similar alphabet-size reduction by similarly establishing strong bounds on the probability that certain random rectangular matrices are full rank. To accomplish this in our insdel context, our proof combines the random matrix techniques from list-decoding with structural properties of Longest Common Subsequences.
Cite as

Roni Con, Zeyu Guo, Ray Li, and Zihan Zhang. Random Reed-Solomon Codes Achieve the Half-Singleton Bound for Insertions and Deletions over Linear-Sized Alphabets. In 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 334, pp. 60:1-60:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{con_et_al:LIPIcs.ICALP.2025.60,
  author =	{Con, Roni and Guo, Zeyu and Li, Ray and Zhang, Zihan},
  title =	{{Random Reed-Solomon Codes Achieve the Half-Singleton Bound for Insertions and Deletions over Linear-Sized Alphabets}},
  booktitle =	{52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025)},
  pages =	{60:1--60:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-372-0},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{334},
  editor =	{Censor-Hillel, Keren and Grandoni, Fabrizio and Ouaknine, Jo\"{e}l and Puppis, Gabriele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2025.60},
  URN =		{urn:nbn:de:0030-drops-234372},
  doi =		{10.4230/LIPIcs.ICALP.2025.60},
  annote =	{Keywords: coding theory, error-correcting codes, Reed-Solomon codes, insdel, insertion-deletion errors, half-Singleton bound}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2025.4
Ensuring Convergence and Invariants Without Coordination

Authors: Dina Borrego, Nuno Preguiça, Elisa Gonzalez Boix, and Carla Ferreira

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

Abstract
The CAP theorem demonstrates a trade-off between consistency and availability (and, by extension, latency) in systems where network partitions are unavoidable, such as in cloud computing and local-first software. While adopting weak consistency can preserve availability, it may result in inconsistencies that compromise application correctness. Replicated data types provide a principled, coordination-free approach to guarantee convergence but do not consider application invariants. Existing methods for maintaining invariants in replicated systems either rely on coordination - undermining the benefits of weak consistency - or suffer from limited applicability. This paper introduces the No-Op framework, a generic approach for enforcing consistency without coordination while guaranteeing both convergence and invariant preservation. The core idea of the No-Op approach is to resolve conflicts among concurrent operations by prioritising one operation over the other according to programmer-defined conflict resolution policies. This prioritisation transforms the less-preferred operation into a no-side-effect operation, ensuring conflict-free execution. We formalise the model underlying the No-Op framework and introduce a replication protocol built upon it, accompanied by a formal proof of correctness for both the framework and the protocol. Furthermore, we demonstrate the framework’s applicability by showcasing the design of widely used replicated data types and the preservation of a wide range of application invariants.
Cite as

Dina Borrego, Nuno Preguiça, Elisa Gonzalez Boix, and Carla Ferreira. Ensuring Convergence and Invariants Without Coordination. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 4:1-4:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{borrego_et_al:LIPIcs.ECOOP.2025.4,
  author =	{Borrego, Dina and Pregui\c{c}a, Nuno and Gonzalez Boix, Elisa and Ferreira, Carla},
  title =	{{Ensuring Convergence and Invariants Without Coordination}},
  booktitle =	{39th European Conference on Object-Oriented Programming (ECOOP 2025)},
  pages =	{4:1--4: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.4},
  URN =		{urn:nbn:de:0030-drops-232978},
  doi =		{10.4230/LIPIcs.ECOOP.2025.4},
  annote =	{Keywords: distributed systems, conflict resolution, RDTs, invariant preservation}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2025.12
Automatic Goal Clone Detection in Rocq

Authors: Ali Ghanbari

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

Abstract
Proof engineering in Rocq is a labor-intensive process, and as proof developments grow in size, redundancy and maintainability become challenges. One such redundancy is goal cloning, i.e., proving α-equivalent goals multiple times, leading to wasted effort and bloated proof scripts. In this paper, we introduce clone-finder, a novel technique for detecting goal clones in Rocq proofs. By leveraging the formal notion of α-equivalence for Gallina terms, clone-finder systematically identifies duplicated proof goals across large Rocq codebases. We evaluate clone-finder on 40 real-world Rocq projects from the CoqGym dataset. Our results reveal that each project contains an average of 27.73 instances of goal clone. We observed that the clones can be categorized as either exact goal duplication, generalization, or α-equivalent goals with different proofs, each signifying varying levels duplicate effort. Our findings highlight significant untapped potential for proof reuse in Rocq-based formal verification projects, paving the way for future improvements in automated proof engineering.
Cite as

Ali Ghanbari. Automatic Goal Clone Detection in Rocq. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 12:1-12:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{ghanbari:LIPIcs.ECOOP.2025.12,
  author =	{Ghanbari, Ali},
  title =	{{Automatic Goal Clone Detection in Rocq}},
  booktitle =	{39th European Conference on Object-Oriented Programming (ECOOP 2025)},
  pages =	{12:1--12:19},
  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.12},
  URN =		{urn:nbn:de:0030-drops-233055},
  doi =		{10.4230/LIPIcs.ECOOP.2025.12},
  annote =	{Keywords: Clone Detection, Goal, Proof, Rocq, Gallina}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2025.11
Contract Usage and Evolution in Android Mobile Applications

Authors: David R. Ferreira, Alexandra Mendes, João F. Ferreira, and Carolina Carreira

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

Abstract
Contracts and assertions are effective methods to enhance software quality by enforcing preconditions, postconditions, and invariants. Previous research has demonstrated the value of contracts in traditional software development. However, the adoption and impact of contracts in the context of mobile app development, particularly of Android apps, remain unexplored. To address this, we present the first large-scale empirical study on the use of contracts in Android apps, written in Java or Kotlin. We consider contract elements divided into five categories: conditional runtime exceptions, APIs, annotations, assertions, and other. We analyzed 2,390 Android apps from the F-Droid repository and processed 52,977 KLOC to determine 1) how and to what extent contracts are used, 2) which language features are used to denote contracts, 3) how contract usage evolves from the first to the last version, and 4) whether contracts are used safely in the context of program evolution and inheritance. Our findings include: 1) although most apps do not specify contracts, annotation-based approaches are the most popular; 2) apps that use contracts continue to use them in later versions, but the number of methods increases at a higher rate than the number of contracts; and 3) there are potentially unsafe specification changes when apps evolve and in subtyping relationships, which indicates a lack of specification stability. Finally, we present a qualitative study that gathers challenges faced by practitioners when using contracts and that validates our recommendations.
Cite as

David R. Ferreira, Alexandra Mendes, João F. Ferreira, and Carolina Carreira. Contract Usage and Evolution in Android Mobile Applications. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 11:1-11:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{ferreira_et_al:LIPIcs.ECOOP.2025.11,
  author =	{Ferreira, David R. and Mendes, Alexandra and Ferreira, Jo\~{a}o F. and Carreira, Carolina},
  title =	{{Contract Usage and Evolution in Android Mobile Applications}},
  booktitle =	{39th European Conference on Object-Oriented Programming (ECOOP 2025)},
  pages =	{11:1--11:30},
  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.11},
  URN =		{urn:nbn:de:0030-drops-233041},
  doi =		{10.4230/LIPIcs.ECOOP.2025.11},
  annote =	{Keywords: Contracts, Design by Contract, DbC, Android, Java, Kotlin}
}
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.ECOOP.2023.4
Hoogle⋆: Constants and λ-abstractions in Petri-net-based Synthesis using Symbolic Execution

Authors: Henrique Botelho Guerra, João F. Ferreira, and João Costa Seco

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

Abstract
Type-directed component-based program synthesis is the task of automatically building a function with applications of available components and whose type matches a given goal type. Existing approaches to component-based synthesis, based on classical proof search, cannot deal with large sets of components. Recently, Hoogle+, a component-based synthesizer for Haskell, overcomes this issue by reducing the search problem to a Petri-net reachability problem. However, Hoogle+ cannot synthesize constants nor λ-abstractions, which limits the problems that it can solve. We present Hoogle⋆, an extension to Hoogle+ that brings constants and λ-abstractions to the search space, in two independent steps. First, we introduce the notion of wildcard component, a component that matches all types. This enables the algorithm to produce incomplete functions, i.e., functions containing occurrences of the wildcard component. Second, we complete those functions, by replacing each occurrence with constants or custom-defined λ-abstractions. We have chosen to find constants by means of an inference algorithm: we present a new unification algorithm based on symbolic execution that uses the input-output examples supplied by the user to compute substitutions for the occurrences of the wildcard. When compared to Hoogle+, Hoogle⋆ can solve more kinds of problems, especially problems that require the generation of constants and λ-abstractions, without performance degradation.
Cite as

Henrique Botelho Guerra, João F. Ferreira, and João Costa Seco. Hoogle⋆: Constants and λ-abstractions in Petri-net-based Synthesis using Symbolic Execution. In 37th European Conference on Object-Oriented Programming (ECOOP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 263, pp. 4:1-4:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{botelhoguerra_et_al:LIPIcs.ECOOP.2023.4,
  author =	{Botelho Guerra, Henrique and Ferreira, Jo\~{a}o F. and Costa Seco, Jo\~{a}o},
  title =	{{Hoogle⋆: Constants and \lambda-abstractions in Petri-net-based Synthesis using Symbolic Execution}},
  booktitle =	{37th European Conference on Object-Oriented Programming (ECOOP 2023)},
  pages =	{4:1--4:28},
  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.4},
  URN =		{urn:nbn:de:0030-drops-181974},
  doi =		{10.4230/LIPIcs.ECOOP.2023.4},
  annote =	{Keywords: Type-directed, component-based, program synthesis, symbolic execution, unification, Haskell}
}
Document
Artifact
DOI: 10.4230/DARTS.9.2.20
Hoogle⋆: Constants and λ-abstractions in Petri-net-based Synthesis using Symbolic Execution (Artifact)

Authors: Henrique Botelho Guerra, João F. Ferreira, and João Costa Seco

Published in: DARTS, Volume 9, Issue 2, Special Issue of the 37th European Conference on Object-Oriented Programming (ECOOP 2023)

Abstract
Type-directed component-based program synthesis is the task of automatically building a function with applications of available components and whose type matches a given goal type. Existing approaches to component-based synthesis, based on classical proof search, cannot deal with large sets of components. Recently, Hoogle+, a component-based synthesizer for Haskell, overcomes this issue by reducing the search problem to a Petri-net reachability problem. However, Hoogle+ cannot synthesize constants nor λ-abstractions, which limits the problems that it can solve. We present Hoogle⋆, an extension to Hoogle+ that brings constants and λ-abstractions to the search space, in two independent steps. First, we introduce the notion of wildcard component, a component that matches all types. This enables the algorithm to produce incomplete functions, i.e., functions containing occurrences of the wildcard component. Second, we complete those functions, by replacing each occurrence with constants or custom-defined λ-abstractions. We have chosen to find constants by means of an inference algorithm: we present a new unification algorithm based on symbolic execution that uses the input-output examples supplied by the user to compute substitutions for the occurrences of the wildcard. When compared to Hoogle+, Hoogle⋆ can solve more kinds of problems, especially problems that require the generation of constants and λ-abstractions, without performance degradation. The artifact contains the source code of Hoogle⋆, as well as scripts to reproduce the evaluation done in the paper.
Cite as

Henrique Botelho Guerra, João F. Ferreira, and João Costa Seco. Hoogle⋆: Constants and λ-abstractions in Petri-net-based Synthesis using Symbolic Execution (Artifact). In Special Issue of the 37th European Conference on Object-Oriented Programming (ECOOP 2023). Dagstuhl Artifacts Series (DARTS), Volume 9, Issue 2, pp. 20:1-20:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@Article{botelhoguerra_et_al:DARTS.9.2.20,
  author =	{Botelho Guerra, Henrique and Ferreira, Jo\~{a}o F. and Costa Seco, Jo\~{a}o},
  title =	{{Hoogle⋆: Constants and \lambda-abstractions in Petri-net-based Synthesis using Symbolic Execution (Artifact)}},
  pages =	{20:1--20:3},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2023},
  volume =	{9},
  number =	{2},
  editor =	{Botelho Guerra, Henrique and Ferreira, Jo\~{a}o F. and Costa Seco, Jo\~{a}o},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.9.2.20},
  URN =		{urn:nbn:de:0030-drops-182609},
  doi =		{10.4230/DARTS.9.2.20},
  annote =	{Keywords: Type-directed, component-based, program synthesis, symbolic execution, unification, Haskell}
}
Document
DOI: 10.4230/OASIcs.SLATE.2021.6
DataGen: JSON/XML Dataset Generator

Authors: Filipa Alves dos Santos, Hugo André Coelho Cardoso, João da Cunha e Costa, Válter Ferreira Picas Carvalho, and José Carlos Ramalho

Published in: OASIcs, Volume 94, 10th Symposium on Languages, Applications and Technologies (SLATE 2021)

Abstract
In this document we describe the steps towards DataGen implementation. DataGen is a versatile and powerful tool that allows for quick prototyping and testing of software applications, since currently too few solutions offer both the complexity and scalability necessary to generate adequate datasets in order to feed a data API or a more complex APP enabling those applications testing with appropriate data volume and data complexity. DataGen core is a Domain Specific Language (DSL) that was created to specify datasets. This language suffered several updates: repeating fields (with no limit), fuzzy fields (statistically generated), lists, highorder functions over lists, custom made transformation functions. The final result is a complex algebra that allows the generation of very complex datasets coping with very complex requirements. Throughout the paper we will give several examples of the possibilities. After generating a dataset DataGen gives the user the possibility to generate a RESTFull data API with that dataset, creating a running prototype. This solution has already been used in real life cases, described with more detail throughout the paper, in which it was able to create the intended datasets successfully. These allowed the application’s performance to be tested and for the right adjustments to be made. The tool is currently being deployed for general use.
Cite as

Filipa Alves dos Santos, Hugo André Coelho Cardoso, João da Cunha e Costa, Válter Ferreira Picas Carvalho, and José Carlos Ramalho. DataGen: JSON/XML Dataset Generator. In 10th Symposium on Languages, Applications and Technologies (SLATE 2021). Open Access Series in Informatics (OASIcs), Volume 94, pp. 6:1-6:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{santos_et_al:OASIcs.SLATE.2021.6,
  author =	{Santos, Filipa Alves dos and Cardoso, Hugo Andr\'{e} Coelho and da Cunha e Costa, Jo\~{a}o and Carvalho, V\'{a}lter Ferreira Picas and Ramalho, Jos\'{e} Carlos},
  title =	{{DataGen: JSON/XML Dataset Generator}},
  booktitle =	{10th Symposium on Languages, Applications and Technologies (SLATE 2021)},
  pages =	{6:1--6:14},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-202-0},
  ISSN =	{2190-6807},
  year =	{2021},
  volume =	{94},
  editor =	{Queir\'{o}s, Ricardo and Pinto, M\'{a}rio and Sim\~{o}es, Alberto and Portela, Filipe and Pereira, Maria Jo\~{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.2021.6},
  URN =		{urn:nbn:de:0030-drops-144239},
  doi =		{10.4230/OASIcs.SLATE.2021.6},
  annote =	{Keywords: JSON, XML, Data Generation, Open Source, REST API, Strapi, JavaScript, Node.js, Vue.js, Scalability, Fault Tolerance, Dataset, DSL, PEG.js, MongoDB}
}
Document
Short Paper
DOI: 10.4230/OASIcs.SLATE.2020.16
Assessing Factoid Question-Answer Generation for Portuguese (Short Paper)

Authors: João Ferreira, Ricardo Rodrigues, and Hugo Gonçalo Oliveira

Published in: OASIcs, Volume 83, 9th Symposium on Languages, Applications and Technologies (SLATE 2020)

Abstract
We present work on the automatic generation of question-answer pairs in Portuguese, useful, for instance, for populating the knowledge-base of question-answering systems. This includes: (i) a new corpus of close to 600 factoid sentences, manually created from an existing corpus of questions and answers, used as our benchmark; (ii) two approaches for the automatic generation of question-answer pairs, which can be seen as baselines; (iii) results of those approaches in the corpus.
Cite as

João Ferreira, Ricardo Rodrigues, and Hugo Gonçalo Oliveira. Assessing Factoid Question-Answer Generation for Portuguese (Short Paper). In 9th Symposium on Languages, Applications and Technologies (SLATE 2020). Open Access Series in Informatics (OASIcs), Volume 83, pp. 16:1-16:9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{ferreira_et_al:OASIcs.SLATE.2020.16,
  author =	{Ferreira, Jo\~{a}o and Rodrigues, Ricardo and Gon\c{c}alo Oliveira, Hugo},
  title =	{{Assessing Factoid Question-Answer Generation for Portuguese}},
  booktitle =	{9th Symposium on Languages, Applications and Technologies (SLATE 2020)},
  pages =	{16:1--16:9},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-165-8},
  ISSN =	{2190-6807},
  year =	{2020},
  volume =	{83},
  editor =	{Sim\~{o}es, Alberto and Henriques, Pedro Rangel and Queir\'{o}s, Ricardo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.SLATE.2020.16},
  URN =		{urn:nbn:de:0030-drops-130298},
  doi =		{10.4230/OASIcs.SLATE.2020.16},
  annote =	{Keywords: Question-Answer Generation, Corpus, NLP, Portuguese}
}
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}
}
Document
DOI: 10.4230/OASIcs.ICPEC.2020.7
CodeCubes: Coding with Augmented Reality

Authors: Bárbara Cleto, Cristina Sylla, Luís Ferreira, and João Martinho Moura

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

Abstract
CodeCubes is interface that uses Augmented Reality to stimulate Computational Thinking in young students. The visual programming blocks are replaced by paper cubes that have an Augmented Reality marker on each face. Each marker represents a programming instruction. The game is composed of three levels. It consists of programming a car course in a racetrack, driving from the start to the final goal. Code Cubes takes advantage of the physicality offered by Augmented Reality technology. We present the design and development of the game, focusing on its main characteristics and describing the various development stages. We also present the first results obtained by exploring Code Cubes. The results were positive, showing the potential of Augmented Reality interfaces in learning scenarios.
Cite as

Bárbara Cleto, Cristina Sylla, Luís Ferreira, and João Martinho Moura. CodeCubes: Coding with Augmented Reality. In First International Computer Programming Education Conference (ICPEC 2020). Open Access Series in Informatics (OASIcs), Volume 81, pp. 7:1-7:9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{cleto_et_al:OASIcs.ICPEC.2020.7,
  author =	{Cleto, B\'{a}rbara and Sylla, Cristina and Ferreira, Lu{\'\i}s and Moura, Jo\~{a}o Martinho},
  title =	{{CodeCubes: Coding with Augmented Reality}},
  booktitle =	{First International Computer Programming Education Conference (ICPEC 2020)},
  pages =	{7:1--7:9},
  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.7},
  URN =		{urn:nbn:de:0030-drops-122943},
  doi =		{10.4230/OASIcs.ICPEC.2020.7},
  annote =	{Keywords: Tangible Interfaces, Augmented Reality, Computational Thinking, Games}
}
  • Refine by Type
  • 21 Document/PDF
  • 9 Document/HTML

  • Refine by Publication Year
  • 2 2026
  • 7 2025
  • 2 2023
  • 1 2021
  • 3 2020
  • Show More...

  • Refine by Author
  • 3 Ferreira, João F.
  • 3 Henriques, Pedro Rangel
  • 2 Botelho Guerra, Henrique
  • 2 Costa Seco, João
  • 2 Ferreira, João
  • Show More...

  • Refine by Series/Journal
  • 7 LIPIcs
  • 13 OASIcs
  • 1 DARTS

  • Refine by Classification
  • 3 Software and its engineering → Automatic programming
  • 2 Computing methodologies → Mixed / augmented reality
  • 2 Computing methodologies → Natural language processing
  • 2 Software and its engineering → Domain specific languages
  • 2 Theory of computation → Automated reasoning
  • Show More...

  • Refine by Keyword
  • 2 Augmented Reality
  • 2 Haskell
  • 2 NLP
  • 2 Type-directed
  • 2 XML
  • 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