Cookies Policy
We use cookies to improve our site and your experience. By continuing to browse our site you accept our cookie policy. Find out More
Close
  • Menu
About

About

I am a senior member of the Association for Computing Machinery, an Associate Professor at the Department of Informatics of the University of Minho, and a researcher at HASLab/INESC TEC. I obtained my degree of Docteur de L'Ecole Polytechnique (Paris) in 2001 and my Habilitation from the University of Minho in 2015. In the past I have worked on linear logic and functional programming; more recently my work focused on deductive program verification and model checking of software, which were the subjects of the AVIACC project that I coordinated. I am one of the authors of the textbook "Rigorous Software Development: an Introduction to Program Verification". 

Interest
Topics
Details

Details

  • Name

    Jorge Sousa Pinto
  • Cluster

    Computer Science
  • Role

    Research Coordinator
  • Since

    01st November 2011
Publications

2018

K-Taint: An Executable Rewriting Logic Semantics for Taint Analysis in the K Framework

Authors
Alam, MI; Halder, R; Goswami, H; Pinto, JS;

Publication
Proceedings of the 13th International Conference on Evaluation of Novel Approaches to Software Engineering, ENASE 2018, Funchal, Madeira, Portugal, March 23-24, 2018.

Abstract

2018

Runtime verification of autopilot systems using a fragment of MTL-?

Authors
Pedro, AD; Pinto, JS; Pereira, D; Pinho, LM;

Publication
International Journal on Software Tools for Technology Transfer

Abstract
Current real-time embedded systems development frameworks lack support for the verification of properties using explicit time where counting time (i.e., durations) may play an important role in the development process. Focusing on the real-time constraints inherent to these systems, we present a framework that addresses the specification of duration properties for runtime verification by employing a fragment of metric temporal logic with durations. We also provide an overview of the framework, the synthesis tools, and the library to support monitoring properties for real-time systems developed in C++11. The results obtained provide clear evidence of the feasibility and advantages of employing a duration-sensitive formalism to increase the dependability of avionic controller systems such as the PX4 and the Ardupilot flight stacks. © 2017 Springer-Verlag GmbH Germany

2018

A Generalized Approach to Verification Condition Generation

Authors
Lourenço, CB; Frade, MJ; Nakajima, S; Pinto, JS;

Publication
2018 IEEE 42nd Annual Computer Software and Applications Conference, COMPSAC 2018, Tokyo, Japan, 23-27 July 2018, Volume 1

Abstract

2018

A Generalized Approach to Verification Condition Generation

Authors
Belo Lourenco, C; Frade, MJ; Nakajima, S; Sousa Pinto, J;

Publication
Proceedings - International Computer Software and Applications Conference

Abstract
In a world where many human lives depend on the correct behavior of software systems, program verification assumes a crucial role. Many verification tools rely on an algorithm that generates verification conditions (VCs) from code annotated with properties to be checked. In this paper, we revisit two major methods that are widely used to produce VCs: predicate transformers (used mostly by deductive verification tools) and the conditional normal form transformation (used in bounded model checking of software). We identify three different aspects in which the methods differ (logical encoding of control flow, use of contexts, and semantics of asserts), and show that, since they are orthogonal, they can be freely combined. This results in six new hybrid verification condition generators (VCGens), which together with the fundamental methods constitute what we call the VCGen cube. We consider two optimizations implemented in major program verification tools and show that each of them can in fact be applied to an entire face of the cube, resulting in optimized versions of the six hybrid VCGens. Finally, we compare all VCGens empirically using a number of benchmarks. Although the results do not indicate absolute superiority of any given method, they do allow us to identify interesting patterns. © 2018 IEEE.

2017

SMT-based schedulability analysis using RMTL-?

Authors
Matos Pedro, Ad; Pereira, D; Pinho, LM; Pinto, JS;

Publication
SIGBED Review

Abstract

Supervised
thesis

2015

Dynamic contracts for verification and enforcement of real-time systems properties

Author
André Matos Pedro

Institution
UM

2015

Software Verification and Defect Analysis

Author
Claudio Filipe Belo Silva Lourenço

Institution
UM