8 Search Results for "Lopes, Nuno"


Document
Bit-Precise Reasoning with Parametric Bit-Vectors

Authors: Zvika Berger, Yoni Zohar, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark Barrett, and Cesare Tinelli

Published in: LIPIcs, Volume 341, 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)


Abstract
The SMT-LIB theory of bit-vectors is restricted to bit-vectors of fixed width. However, several important applications can benefit from reasoning about bit-vectors of symbolic widths, i.e., parametric bit-vectors. Recent work has introduced an approach for solving formulas over parametric bit-vectors, via an eager translation to quantified integer arithmetic with uninterpreted functions. The approach was shown to be successful for several applications, including the bit-width independent verification of compiler optimizations, invertibility conditions, and rewrite rules. We extend and improve that approach in several aspects. Theoretically, we improve expressiveness by defining a new theory of parametric bit-vectors that supports more operators and allows reasoning about the bit-widths themselves. Algorithmically, we introduce a lazy algorithm that avoids the use of uninterpreted functions and quantified axioms for them. Empirically, we show a significant improvement by implementing and evaluating our approach, and comparing it experimentally to the previous one.

Cite as

Zvika Berger, Yoni Zohar, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark Barrett, and Cesare Tinelli. Bit-Precise Reasoning with Parametric Bit-Vectors. In 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 341, pp. 4:1-4:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)


Copy BibTex To Clipboard

@InProceedings{berger_et_al:LIPIcs.SAT.2025.4,
  author =	{Berger, Zvika and Zohar, Yoni and Niemetz, Aina and Preiner, Mathias and Reynolds, Andrew and Barrett, Clark and Tinelli, Cesare},
  title =	{{Bit-Precise Reasoning with Parametric Bit-Vectors}},
  booktitle =	{28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)},
  pages =	{4:1--4:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-381-2},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{341},
  editor =	{Berg, Jeremias and Nordstr\"{o}m, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2025.4},
  URN =		{urn:nbn:de:0030-drops-237385},
  doi =		{10.4230/LIPIcs.SAT.2025.4},
  annote =	{Keywords: Satisfiability Modulo Theories, Bit-precise Reasoning, Parametric Bit-vectors}
}
Document
CVTool: Automating Content Variants of CVs

Authors: Julio Beites Gonçalves, Maria João Varanda Pereira, and Pedro Rangel Henriques

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


Abstract
As academic professionals, we frequently need to create different versions of our CVs for project applications, career evaluations, or competitions. These versions may be chronologically structured or skill-oriented, covering specific periods and written in various languages. Even when using a LaTeX document as a base, numerous modifications are required each time an updated CV version is requested for a specific purpose. The primary objective of the project reported in this paper is to design and implement a web-based system (CVTool) that simplifies the management of LaTeX CV content while ensuring flexibility. The CVTool is built on a domain-specific language that enables the creation of various filters, allowing for the automatic content adjustment while preserving the original format. Information is extracted from the LaTeX document, and users can specify the sections, dates, skills they want to highlight, and the language in which the CV should be generated. Since the approach relies on an internal data representation derived from the original LaTeX document, it offers users the flexibility to manage content efficiently and extract the necessary information with ease.

Cite as

Julio Beites Gonçalves, Maria João Varanda Pereira, and Pedro Rangel Henriques. CVTool: Automating Content Variants of CVs. In 14th Symposium on Languages, Applications and Technologies (SLATE 2025). Open Access Series in Informatics (OASIcs), Volume 135, pp. 5:1-5:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)


Copy BibTex To Clipboard

@InProceedings{goncalves_et_al:OASIcs.SLATE.2025.5,
  author =	{Gon\c{c}alves, Julio Beites and Pereira, Maria Jo\~{a}o Varanda and Henriques, Pedro Rangel},
  title =	{{CVTool: Automating Content Variants of CVs}},
  booktitle =	{14th Symposium on Languages, Applications and Technologies (SLATE 2025)},
  pages =	{5:1--5:14},
  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.5},
  URN =		{urn:nbn:de:0030-drops-236855},
  doi =		{10.4230/OASIcs.SLATE.2025.5},
  annote =	{Keywords: Latex CV, CV Versioning, DSL, CV Parsing, CV Templates}
}
Document
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
Survey
How Does Knowledge Evolve in Open Knowledge Graphs?

Authors: Axel Polleres, Romana Pernisch, Angela Bonifati, Daniele Dell'Aglio, Daniil Dobriy, Stefania Dumbrava, Lorena Etcheverry, Nicolas Ferranti, Katja Hose, Ernesto Jiménez-Ruiz, Matteo Lissandrini, Ansgar Scherp, Riccardo Tommasini, and Johannes Wachs

Published in: TGDK, Volume 1, Issue 1 (2023): Special Issue on Trends in Graph Data and Knowledge. Transactions on Graph Data and Knowledge, Volume 1, Issue 1


Abstract
Openly available, collaboratively edited Knowledge Graphs (KGs) are key platforms for the collective management of evolving knowledge. The present work aims t o provide an analysis of the obstacles related to investigating and processing specifically this central aspect of evolution in KGs. To this end, we discuss (i) the dimensions of evolution in KGs, (ii) the observability of evolution in existing, open, collaboratively constructed Knowledge Graphs over time, and (iii) possible metrics to analyse this evolution. We provide an overview of relevant state-of-the-art research, ranging from metrics developed for Knowledge Graphs specifically to potential methods from related fields such as network science. Additionally, we discuss technical approaches - and their current limitations - related to storing, analysing and processing large and evolving KGs in terms of handling typical KG downstream tasks.

Cite as

Axel Polleres, Romana Pernisch, Angela Bonifati, Daniele Dell'Aglio, Daniil Dobriy, Stefania Dumbrava, Lorena Etcheverry, Nicolas Ferranti, Katja Hose, Ernesto Jiménez-Ruiz, Matteo Lissandrini, Ansgar Scherp, Riccardo Tommasini, and Johannes Wachs. How Does Knowledge Evolve in Open Knowledge Graphs?. In Special Issue on Trends in Graph Data and Knowledge. Transactions on Graph Data and Knowledge (TGDK), Volume 1, Issue 1, pp. 11:1-11:59, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)


Copy BibTex To Clipboard

@Article{polleres_et_al:TGDK.1.1.11,
  author =	{Polleres, Axel and Pernisch, Romana and Bonifati, Angela and Dell'Aglio, Daniele and Dobriy, Daniil and Dumbrava, Stefania and Etcheverry, Lorena and Ferranti, Nicolas and Hose, Katja and Jim\'{e}nez-Ruiz, Ernesto and Lissandrini, Matteo and Scherp, Ansgar and Tommasini, Riccardo and Wachs, Johannes},
  title =	{{How Does Knowledge Evolve in Open Knowledge Graphs?}},
  journal =	{Transactions on Graph Data and Knowledge},
  pages =	{11:1--11:59},
  year =	{2023},
  volume =	{1},
  number =	{1},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/TGDK.1.1.11},
  URN =		{urn:nbn:de:0030-drops-194855},
  doi =		{10.4230/TGDK.1.1.11},
  annote =	{Keywords: KG evolution, temporal KG, versioned KG, dynamic KG}
}
Document
OMT, a Web-Based Tool for Ontology Matching

Authors: João Rodrigues Gomes, Alda Lopes Gançarski, and Pedro Rangel Henriques

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


Abstract
In recent years ontologies have become an integral part of storing information in a structured and formal manner and a way of sharing said information. With this rise in usage, it was only a matter of time before different people wrote distinct ontologies to represent the same knowledge domain. The area of Ontology Matching was created with the purpose of finding correspondences between different ontologies that represented information in the same domain area. This paper starts with a study of already existing ontology matching methods in order to understand the existing techniques, focusing on the advantages and disadvantages of each one. Then, we propose an approach and an architecture to develop a new web-based tool using the knowledge acquired during the bibliographic research. The paper also includes the presentation of a prototype of the proposed tool, called OMT.

Cite as

João Rodrigues Gomes, Alda Lopes Gançarski, and Pedro Rangel Henriques. OMT, a Web-Based Tool for Ontology Matching. In 11th Symposium on Languages, Applications and Technologies (SLATE 2022). Open Access Series in Informatics (OASIcs), Volume 104, pp. 8:1-8:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)


Copy BibTex To Clipboard

@InProceedings{gomes_et_al:OASIcs.SLATE.2022.8,
  author =	{Gomes, Jo\~{a}o Rodrigues and Gan\c{c}arski, Alda Lopes and Henriques, Pedro Rangel},
  title =	{{OMT, a Web-Based Tool for Ontology Matching}},
  booktitle =	{11th Symposium on Languages, Applications and Technologies (SLATE 2022)},
  pages =	{8:1--8:12},
  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.8},
  URN =		{urn:nbn:de:0030-drops-167547},
  doi =		{10.4230/OASIcs.SLATE.2022.8},
  annote =	{Keywords: Ontology, Ontology Matching, Ontology Alignment}
}
Document
Large Semantic Graph Summarization Using Namespaces

Authors: Ana Rita Santos Lopes da Costa, André Santos, and José Paulo Leal

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


Abstract
We propose an approach to summarize large semantics graphs using namespaces. Semantic graphs based on the Resource Description Framework (RDF) use namespaces on their serializations. Although these namespaces are not part of RDF semantics, they have intrinsic meaning. Based on this insight, we use namespaces to create summary graphs of reduced size, more amenable to be visualized. In the summarization, object literals are also reduced to their data type and the blank nodes to a group of their own. The visualization created for the summary graph aims to give insight of the original large graph. This paper describes the proposed approach and reports on the results obtained with representative large semantic graphs.

Cite as

Ana Rita Santos Lopes da Costa, André Santos, and José Paulo Leal. Large Semantic Graph Summarization Using Namespaces. In 11th Symposium on Languages, Applications and Technologies (SLATE 2022). Open Access Series in Informatics (OASIcs), Volume 104, pp. 12:1-12:9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)


Copy BibTex To Clipboard

@InProceedings{dacosta_et_al:OASIcs.SLATE.2022.12,
  author =	{da Costa, Ana Rita Santos Lopes and Santos, Andr\'{e} and Leal, Jos\'{e} Paulo},
  title =	{{Large Semantic Graph Summarization Using Namespaces}},
  booktitle =	{11th Symposium on Languages, Applications and Technologies (SLATE 2022)},
  pages =	{12:1--12:9},
  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.12},
  URN =		{urn:nbn:de:0030-drops-167585},
  doi =		{10.4230/OASIcs.SLATE.2022.12},
  annote =	{Keywords: Semantic graph, RDF, namespaces, reification}
}
Document
A Logic Programming approach for Access Control over RDF

Authors: Nuno Lopes, Sabrina Kirrane, Antoine Zimmermann, Axel Polleres, and Alessandra Mileo

Published in: LIPIcs, Volume 17, Technical Communications of the 28th International Conference on Logic Programming (ICLP'12) (2012)


Abstract
The Resource Description Framework (RDF) is an interoperable data representation format suitable for interchange and integration of data, especially in Open Data contexts. However, RDF is also becoming increasingly attractive in scenarios involving sensitive data, where data protection is a major concern. At its core, RDF does not support any form of access control and current proposals for extending RDF with access control do not fit well with the RDF representation model. Considering an enterprise scenario, we present a modelling that caters for access control over the stored RDF data in an intuitive and transparent manner. For this paper we rely on Annotated RDF, which introduces concepts from Annotated Logic Programming into RDF. Based on this model of the access control annotation domain, we propose a mechanism to manage permissions via application-specific logic rules. Furthermore, we illustrate how our Annotated Query Language (AnQL) provides a secure way to query this access control annotated RDF data.

Cite as

Nuno Lopes, Sabrina Kirrane, Antoine Zimmermann, Axel Polleres, and Alessandra Mileo. A Logic Programming approach for Access Control over RDF. In Technical Communications of the 28th International Conference on Logic Programming (ICLP'12). Leibniz International Proceedings in Informatics (LIPIcs), Volume 17, pp. 381-392, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)


Copy BibTex To Clipboard

@InProceedings{lopes_et_al:LIPIcs.ICLP.2012.381,
  author =	{Lopes, Nuno and Kirrane, Sabrina and Zimmermann, Antoine and Polleres, Axel and Mileo, Alessandra},
  title =	{{A Logic Programming approach for Access Control over RDF}},
  booktitle =	{Technical Communications of the 28th International Conference on Logic Programming (ICLP'12)},
  pages =	{381--392},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-43-9},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{17},
  editor =	{Dovier, Agostino and Santos Costa, V{\'\i}tor},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICLP.2012.381},
  URN =		{urn:nbn:de:0030-drops-36384},
  doi =		{10.4230/LIPIcs.ICLP.2012.381},
  annote =	{Keywords: Logic Programming, Annotation, Access Control, RDF}
}
Document
Learning Spaces for Knowledge Generation

Authors: Nuno Oliveira, Maria João Varanda Pereira, Alda Lopes Gancarski, and Pedro Rangel Henriques

Published in: OASIcs, Volume 21, 1st Symposium on Languages, Applications and Technologies (2012)


Abstract
As the Internet is becoming the main point for information access, Libraries, Museums and similar Institutions are preserving their collections as digital object repositories. In that way, the important information associated with digital objects may be delivered as Internet content over portals equipped with modern interfaces and navigation features. This enables the virtualization of real information exhibition spaces rising new learning paradigms. Geny is a project aiming at defining domain-specific languages and developing tools to generate web-based learning spaces from existent digital object repositories and associated semantic. The motto for Geny is "Generating learning spaces to generate knowledge". Our objective within this project is to use (i) ontologies - one to give semantics to the digital object repository and another to describe the information to exhibit - and (ii) special languages to define the exhibition space, to enable the automatic construction of the learning space supported by a web browser. This paper presents the proposal of the Geny project along with a review of the state of the art concerning learning spaces and their virtualization. Geny is, currently, under appreciation by Fundação para a Ciêencia e a Tecnologia (FCT), the main Portuguese scientific funding institution.

Cite as

Nuno Oliveira, Maria João Varanda Pereira, Alda Lopes Gancarski, and Pedro Rangel Henriques. Learning Spaces for Knowledge Generation. In 1st Symposium on Languages, Applications and Technologies. Open Access Series in Informatics (OASIcs), Volume 21, pp. 175-184, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)


Copy BibTex To Clipboard

@InProceedings{oliveira_et_al:OASIcs.SLATE.2012.175,
  author =	{Oliveira, Nuno and Varanda Pereira, Maria Jo\~{a}o and Gancarski, Alda Lopes and Henriques, Pedro Rangel},
  title =	{{Learning Spaces for Knowledge Generation}},
  booktitle =	{1st Symposium on Languages, Applications and Technologies},
  pages =	{175--184},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-40-8},
  ISSN =	{2190-6807},
  year =	{2012},
  volume =	{21},
  editor =	{Sim\~{o}es, Alberto and Queir\'{o}s, Ricardo and da Cruz, Daniela},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.SLATE.2012.175},
  URN =		{urn:nbn:de:0030-drops-35228},
  doi =		{10.4230/OASIcs.SLATE.2012.175},
  annote =	{Keywords: Learning Spaces, Knowledge Acquisition, Digital Object Repositories, Ontology-based semantic Web-pages Generation}
}
  • Refine by Type
  • 8 Document/PDF
  • 4 Document/HTML

  • Refine by Publication Year
  • 3 2025
  • 1 2023
  • 2 2022
  • 2 2012

  • Refine by Author
  • 3 Henriques, Pedro Rangel
  • 2 Polleres, Axel
  • 1 Barrett, Clark
  • 1 Berger, Zvika
  • 1 Bonifati, Angela
  • Show More...

  • Refine by Series/Journal
  • 3 LIPIcs
  • 4 OASIcs
  • 1 TGDK

  • Refine by Classification
  • 1 Computer systems organization → Availability
  • 1 Computing methodologies → Distributed computing methodologies
  • 1 Computing methodologies → Ontology engineering
  • 1 Information systems → Data streaming
  • 1 Information systems → Graph-based database models
  • Show More...

  • Refine by Keyword
  • 2 RDF
  • 1 Access Control
  • 1 Annotation
  • 1 Bit-precise Reasoning
  • 1 CV Parsing
  • 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