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
Download Photo HD

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

    Research Coordinator
  • Since

    01st November 2011
  • Nationality

    Portugal
  • Contacts

    +351253604440
    jorge.s.pinto@inesctec.pt
Publications

2020

Testing for Race Conditions in Distributed Systems via SMT Solving

Authors
Pereira, JC; Machado, N; Pinto, JS;

Publication
Tests and Proofs - Lecture Notes in Computer Science

Abstract

2019

A Generalized Program Verification Workflow Based on Loop Elimination and SA Form

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

Publication
Proceedings - 2019 IEEE/ACM 7th International Workshop on Formal Methods in Software Engineering, FormaliSE 2019

Abstract
This paper presents a minimal model of the functioning of program verification and property checking tools based on (i) the encoding of loops as non-iterating programs, either conservatively, making use of invariants and assume/assert commands, or in a bounded way; and (ii) the use of an intermediate single-assignment (SA) form. The model captures the basic workflow of tools like Boogie, Why3, or CBMC, building on a clear distinction between operational and axiomatic semantics. This allows us to consider separately the soundness of program annotation, loop encoding, translation into SA form, and VC generation, as well as appropriate notions of completeness for each of these processes. To the best of our knowledge, this is the first formalization of a bounded model checking of software technique, including soundness and completeness proofs using Hoare logic; we also give the first completeness proof of a deductive verification technique based on a conservative encoding of invariant-annotated loops with assume/assert in SA form, as well as the first soundness proof based on a program logic. © 2019 IEEE.

2019

A generalized program verification workflow based on loop elimination and SA form

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

Publication
Proceedings of the 7th International Workshop on Formal Methods in Software Engineering, FormaliSE@ICSE 2019, Montreal, QC, Canada, May 27, 2019.

Abstract

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

Supervised
thesis

2019

Early Validation of System Requirements and Design

Author
Marcelo António Caridade Miranda

Institution
UM

2018

Verificação Funcional de Controladores Arduino

Author
Rafael Alexandre Antunes Barbosa

Institution
UM

2018

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

Author
André de Matos Pedro

Institution
UM

2018

Single-assignment Program Verification

Author
Cláudio Filipe Belo da Silva Lourenço

Institution
UM

2017

Software Verification and Defect Analysis

Author
Cláudio Lourenço

Institution
UM