Cookies Policy
The website need some cookies and similar means to function. If you permit us, we will use those means to collect data on your visits for aggregated statistics to improve our service. Find out More
Accept Reject
  • Menu
About

About

I am an Associate Professor at the Department of Informatics of the University of Minho and a Senior Researcher at HASLab/INESC TEC.

I hold a D.Phill in Computation from The University of Oxford.

My current interests are in  formal aspects of programming, namely the correctness of programs and methods of building correct programs.

For the last 20 years I have been teaching courses on functional and imperative programming as well as a course on algorithms and complexity to undergraduate students at Universidade do Minho.

I am also a member of the MFES (formal methods for software engineering) team in the MSc in Informatics Engineering.

Interest
Topics
Details

Details

  • Name

    José Bernardo Barros
  • Role

    Senior Researcher
  • Since

    01st November 2011
Publications

2012

Assertion-based slicing and slice graphs

Authors
Barros, JB; da Cruz, D; Henriques, PR; Pinto, JS;

Publication
FORMAL ASPECTS OF COMPUTING

Abstract
This paper revisits the idea of slicing programs based on their axiomatic semantics, rather than using criteria based on control/data dependencies. We show how the forward propagation of preconditions and the backward propagation of postconditions can be combined in a new slicing algorithm that is more precise than the existing specification-based algorithms. The algorithm is based on (a) a precise test for removable statements, and (b) the construction of a slice graph, a program control flow graph extended with semantic labels and additional edges that "short-circuit" removable commands. It improves on previous approaches in two aspects: it does not fail to identify removable commands; and it produces the smallest possible slice that can be obtained (in a sense that will be made precise). Iteration is handled through the use of loop invariants and variants to ensure termination. The paper also discusses in detail applications of these forms of slicing, including the elimination of (conditionally) unreachable and dead code, and compares them to other related notions.

2010

Assertion-based slicing and slice graphs

Authors
Barros, JB; Da Cruz, D; Henriques, PR; Pinto, JS;

Publication
Proceedings - Software Engineering and Formal Methods, SEFM 2010

Abstract
This paper revisits the idea of slicing programs based on their axiomatic semantics, rather than using criteria based on control/data dependencies. We show how the forward propagation of preconditions and the backward propagation of post conditions can be combined in a new slicing algorithm that is more precise than the existing specification-based algorithms. The algorithm is based on (i) a precise test for removable statements, and (ii) the construction of a slice graph, a program control flow graph extended with semantic labels. It improves on previous approaches in two aspects: it does not fail to identify removable commands; and it produces the smallest possible slice that can be obtained (in a sense that will be made precise). The paper also reviews in detail, through examples, the ideas behind the use of preconditions and post conditions for slicing programs. © 2010 IEEE.

1996

Semantics of non-terminating rewrite systems using minimal coverings

Authors
Barros, J; Goguen, J;

Publication
COMPUTER SCIENCE LOGIC

Abstract
We propose a new semantics for rewrite systems based on interpreting rewrite rules as inequations between terms in an ordered algebra. In particular, we show that the algebra of normal forms in a terminating system is a uniquely minimal covering of the term algebra. In the non-terminating case, the existence of this minimal covering is established in the completion of an ordered algebra formed by rewriting sequences. We thus generalize the properties of normal forms for non-terminating systems to this minimal covering. These include the existence of normal forms for arbitrary rewrite systems, and their uniqueness far confluent systems, in which case the algebra of normal forms is isomorphic to the canonical quotient algebra associated with the rules when seen as equations. This extends the benefits of algebraic semantics to systems with non-deterministic and non-terminating computations. We first study properties of abstract orders, and then instantiate these to term rewriting systems.

Supervised
thesis

2022

Desenvolvimento de uma plataforma de Fidelização

Author
Hugo Filipe Duarte Carvalho

Institution
UM