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
  • Cluster

    Informática
  • Cargo

    Investigador Coordenador
  • Desde

    01 novembro 2011
003
Publicações

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.

2022

Compiling Quantamorphisms for the IBM Q Experience

Autores
Neri, A; Barbosa, RS; Oliveira, JN;

Publicação
IEEE TRANSACTIONS ON SOFTWARE ENGINEERING

Abstract
Based on the connection between the categorical derivation of classical programs from specifications and a category-theoretic approach to quantum information, this paper contributes to extending the laws of classical program algebra to quantum programming. This aims at building correct-by-construction quantum circuits to be deployed on quantum devices such as those available through the IBM Q Experience. Reversibility is ensured by minimal complements. Such complementation is extended inductively to encompass catamorphisms on lists (vulgo folds), giving rise to the corresponding recursion scheme in reversible computation. The same idea is then applied to the setting of quantum programming, where computation is expressed by unitary transformations. This yields the notion of 'quantamorphism', a structural form of quantum recursion implementing cycles and folds on lists with quantum control flow. By Kleisli correspondence, quantamorphisms can be written as monadic functional programs with quantum parameters. This enables the use of Haskell, a monadic functional programming language, to perform the experimental work. Such calculated quantum programs prepared in Haskell are pushed through Quipper and the Qiskit interface to IBM Q quantum devices. The generated quantum circuits - often quite large - exhibit the predicted behaviour. However, running them on real quantum devices naturally incurs a significant amount of errors. As quantum technology is rapidly evolving, an increase in reliability is likely in the future, allowing for our programs to run more accurately.

2020

Type your matrices for great good: A Haskell library of typed matrices and applications (functional pearl)

Autores
Santos, A; Oliveira, JN;

Publicação
Haskell 2020 - Proceedings of the 13th ACM SIGPLAN International Symposium on Haskell, co-located with ICFP 2020

Abstract
We study a simple inductive data type for representing correct-by-construction matrices. Despite its simplicity, it can be used to implement matrix-manipulation algorithms efficiently and safely, performing in some cases faster than existing alternatives even though the algorithms are written in a direct and purely functional style. A rich collection of laws makes it possible to derive and optimise these algorithms using equational reasoning, avoiding the notorious off-by-one indexing errors when fiddling with matrix dimensions. We demonstrate the usefulness of the data type on several examples, and highlight connections to related topics in category theory. © 2020 ACM.

Teses
supervisionadas

2022

On Conditional Quantum Control

Autor
Daniel Almeida Carvalho

Instituição
UM

2022

Scalable Detection of Security-Vulnerabilities in Source Code,

Autor
Artur Jorge Gomes Queiroz

Instituição
UM

2022

Using Machine Learning to Automatically Infer an Approximation of a Physical System

Autor
Afonso João Borges Cabral Cerejeira da Silva

Instituição
UM

2022

Towards ‘Just Good Enough’ Quantum Programming

Autor
Ana Isabel Carvalho Neri

Instituição
UM

2022

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

Autor
Pedro Faria Durães da Silva

Instituição
UM