Cookies
O website necessita de alguns cookies e outros recursos semelhantes para funcionar. Caso o permita, o INESC TEC irá utilizar cookies para recolher dados sobre as suas visitas, contribuindo, assim, para estatísticas agregadas que permitem melhorar o nosso serviço. Ver mais
Aceitar Rejeitar
  • Menu
Sobre

Sobre

Sou professor no Departamento de Informática da Universidade do Minho e investigador do HASLab / INESC TEC. Também sou membro do IFIP WG 2.1 (Algorithmic Languages and Calculi) e da Associação Formal Methods Europe (FME). Faço parte do conselho editorial da revista Formal Aspects of Computing da Springer.

Meus interesses de investigação estão focados em métodos formais, álgebra de programação (cálculo de programas) e programação funcional. Publiquei recentemente sobre álgebra de relações e sua aplicação à programação. Atualmente, estou a desenvolver uma álgebra linear de programação que quero aplicar à verificação de sistemas de software complexos tolerantes a falhas.

Tópicos
de interesse
Detalhes

Detalhes

  • Nome

    José Nuno Oliveira
  • Cargo

    Investigador Coordenador
  • Desde

    01 novembro 2011
003
Publicações

2023

On difunctions

Autores
Backhouse, R; Oliveira, JN;

Publicação
JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING

Abstract
The notion of a difunction was introduced by Jacques Riguet in 1948. Since then it has played a prominent role in database theory, type theory, program specification and process theory. The theory of difunctions is, however, less known in computing than it perhaps should be. The main purpose of the current paper is to give an account of difunction theory in relation algebra, with the aim of making the topic more mainstream.As is common with many important concepts, there are several different but equivalent characterisations of difunctionality, each with its own strength and practical significance. This paper compares different proofs of the equivalence of the characterisations. A well-known property is that a difunction is a set of completely disjoint rectangles. This property suggests the introduction of the (general) notion of the core of a relation; we use this notion to give a novel and, we believe, illuminating characterisation of difunctionality as a bijection between the classes of certain partial equivalence relations.& COPY; 2023 The Authors. Published by Elsevier Inc. This is an open access article under the CC BY license (http://creativecommons .org /licenses /by /4 .0/).

2023

Why Adjunctions Matter—A Functional Programmer Perspective

Autores
Oliveira, JN;

Publicação
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

Abstract
For the average programmer, adjunctions are (if at all known) more respected than loved. At best, they are regarded as an algebraic device of theoretical interest only, not useful in common practice. This paper is aimed at showing the opposite: that adjunctions underlie most of the work we do as programmers, in particular those using the functional paradigm. However, functions alone are not sufficient to express the whole spectrum of programming, with its dichotomy between specifications—what is (often vaguely) required—and implementations—how what is required is (hopefully well) implemented. For this, one needs to extend functions to relations. Inspired by the pioneering work of Ralf Hinze on “adjoint (un)folds”, the core of the so-called (relational) Algebra of Programming is shown in this paper to arise from adjunctions. Moreover, the paper also shows how to calculate recursive programs from specifications expressed by Galois connections—a special kind of adjunction. Because Galois connections are easier to understand than adjunctions in general, the paper adopts a tutorial style, starting from the former and leading to the latter (a path usually not followed in the literature). The main aim is to reconcile the functional programming community with a concept that is central to software design as a whole, but rarely accepted as such. © 2023, Springer Nature Switzerland AG.

2022

A tribute to Jose Manuel Valenca

Autores
Oliveira, JN; Pinto, JS; Barbosa, LS; Henriques, PR;

Publicação
JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING

Abstract
The present Special Issue of the Journal of Logical and Algebraic Methods in Programming was planned as a tribute to Jose Manuel Esgalhado Valenca on the occasion of his Jubilation. A tribute to a professor, in the deepest sense of the word, a colleague and a friend, but above all to a long and inspiring academic journey that has so profoundly shaped the development of Informatics as a scientific area in Portugal. A scientific area that, as he taught us, needs to be understood broadly: not only as an independent research domain, but also as an educational pillar, a strategy for social and economic development, a foundation for a multifaceted professional career. This preface introduces some steps of such a journey. The Special Issue features a selection of scientific papers written by his collaborators, colleagues and friends, covering the different areas Jose Valenca helped to launch and consolidate in Portugal, namely computational logic, verification and mechanized reasoning, and information security. (c) 2022 Published by Elsevier Inc.

2022

Quantitative relational modelling with QAlloy

Autores
Silva, P; Oliveira, JN; Macedo, N; Cunha, A;

Publicação
Proceedings of the 30th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC/FSE 2022, Singapore, Singapore, November 14-18, 2022

Abstract
Alloy is a popular language and tool for formal software design. A key factor to this popularity is its relational logic, an elegant specification language with a minimal syntax and semantics. However, many software problems nowadays involve both structural and quantitative requirements, and Alloy's relational logic is not well suited to reason about the latter. This paper introduces QAlloy, an extension of Alloy with quantitative relations that add integer quantities to associations between domain elements. Having integers internalised in relations, instead of being explicit domain elements like in standard Alloy, allows quantitative requirements to be specified in QAlloy with a similar elegance to structural requirements, with the side-effect of providing basic dimensional analysis support via the type system. The QAlloy Analyzer also implements an SMT-based engine that enables quantities to be unbounded, thus avoiding many problems that may arise with the current bounded integer semantics of Alloy.

2022

Verification of railway network models with EVEREST

Autores
Martins, J; Fonseca, JM; Costa, R; Campos, JC; Cunha, A; Macedo, N; Oliveira, JN;

Publicação
Proceedings of the 25th International Conference on Model Driven Engineering Languages and Systems, MODELS 2022, Montreal, Quebec, Canada, October 23-28, 2022

Abstract
Models-at different levels of abstraction and pertaining to different engineering views-are central in the design of railway networks, in particular signalling systems. The design of such systems must follow numerous strict rules, which may vary from project to project and require information from different views. This renders manual verification of railway networks costly and error-prone. This paper presents EVEREST, a tool for automating the verification of railway network models that preserves the loosely coupled nature of the design process. To achieve this goal, EVEREST first combines two different views of a railway network model-the topology provided in signalling diagrams containing the functional infrastructure, and the precise coordinates of the elements provided in technical drawings (CAD)-in a unified model stored in the railML standard format. This railML model is then verified against a set of user-defined infrastructure rules, written in a custom modal logic that simplifies the specification of spatial constraints in the network. The violated rules can be visualized both in the signalling diagrams and technical drawings, where the element(s) responsible for the violation are highlighted. EVEREST is integrated in a long-term effort of EFACEC to implement industry-strong tools to automate and formally verify the design of railway solutions. © 2022 ACM.

Teses
supervisionadas

2023

Towards ‘Just Good Enough’ Quantum Programming

Autor
Ana Isabel Carvalho Neri

Instituição
UM

2023

Verificação e descoberta de modelos probabilísticos no Alloy Analyser.

Autor
Pedro Faria Durães da Silva

Instituição
UM

2023

Towards a typed linear algebra formal semantics for spreadsheets

Autor
Rui Filipe Brito Azevedo

Instituição
UM

2023

Functional Programming for Explainable AI

Autor
Gonçalo José Azevedo Esteves

Instituição
UM

2022

Scalable Detection of Security-Vulnerabilities in Source Code,

Autor
Artur Jorge Gomes Queiroz

Instituição
UM