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 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
Publications

2023

A verified VCGen based on dynamic logic: An exercise in meta-verification with Why3

Authors
Frade, MJ; Pinto, JS;

Publication
JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING

Abstract
With the incresasing importance of program verification, an issue that has been receiving more attention is the certification of verification tools, addressing the vernacular question: Who verifies the verifier?. In this paper we approach this meta-verification problem by focusing on a fundamental component of program verifiers: the Verification Conditions Generator (VCGen), responsible for producing a set of proof obligations from a program and a specification. The semantic foundations of VCGens lie in program logics, such as Hoare logic, Dynamic logic, or Separation logic, and related predicate transformers. Dynamic logic is the basis of the KeY system, one of the foremost deductive verifiers, whose logic makes use of the notion of update, which is quite intricate to formalize. In this paper we derive systematically, based on a KeY-style dynamic logic, a correct-by-construction VCGen for a toy programming language. Our workflow covers the entire process, from the logic to the VCGen. It is implemented in the Why3 tool, which is itself a program verifier. We prove the soundness and (an appropriate notion of) completeness of the logic, then define a VCGen for our language and establish its soundness. Dynamic logic is one of a variety of research topics that our dear friend and colleague Luis Soares Barbosa has, over the years, initiated and promoted at the University of Minho. It is a pleasure for us to dedicate this work to him on the occasion of his 60th birthday.

2022

Why3-do: The Way of Harmonious Distributed System Proofs

Authors
Lourenco, CB; Pinto, JS;

Publication
PROGRAMMING LANGUAGES AND SYSTEMS, ESOP 2022

Abstract
We study principles and models for reasoning inductively about properties of distributed systems, based on programmed atomic handlers equipped with contracts. We present the Why3-do library, leveraging a state of the art software verifier for reasoning about distributed systems based on our models. A number of examples involving invariants containing existential and nested quantifiers (including Dijsktra's self-stabilizing systems) illustrate how the library promotes contract-based modular development, abstraction barriers, and automated proofs.

2022

A tribute to Jose Manuel Valenca

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

Publication
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.

2021

A deductive reasoning approach for database applications using verification conditions

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

Publication
JOURNAL OF SYSTEMS AND SOFTWARE

Abstract
Deductive verification has gained paramount attention from both academia and industry. Although intensive research in this direction covers almost all mainstream languages, the research community has paid little attention to the verification of database applications. This paper proposes a comprehensive set of Verification Conditions (VCs) generation techniques from database programs, adapting Symbolic Execution, Conditional Normal Form, and Weakest Precondition. The validity checking of the generated VCs for a database program determines its correctness w.r.t. the annotated database properties. The developed prototype DBverify based on our theoretical foundation allows us to instantiate VC generation from PL/SQL codes, yielding to detailed performance analysis of the three approaches under different circumstances. With respect to the literature, the proposed approach shows its competence to support crucial SQL features (aggregate functions, nested queries, NULL values, and set operations) and the embedding of SQL codes within a host imperative language. For the chosen set of benchmark PL/SQL codes annotated with relevant properties of interest, our experiment shows that only 38% of procedures are correct, while 62% violate either all or part of the annotated properties. The primary cause for the latter case is mostly due to the acceptance of runtime inputs in SQL statements without proper checking.

2020

Testing for Race Conditions in Distributed Systems via SMT Solving

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

Publication
Tests and Proofs - 14th International Conference, TAP@STAF 2020, Bergen, Norway, June 22-23, 2020, Proceedings [postponed]

Abstract
Data races, a condition where two memory accesses to the same memory location occur concurrently, have been shown to be a major source of concurrency bugs in distributed systems. Unfortunately, data races are often triggered by non-deterministic event orderings that are hard to detect when testing complex distributed systems. In this paper, we propose Spider, an automated tool for identifying data races in distributed system traces. Spider encodes the causal relations between the events in the trace as a symbolic constraint model, which is then fed into an SMT solver to check for the presence of conflicting concurrent accesses. To reduce the constraint solving time, Spider employs a pruning technique aimed at removing redundant portions of the trace. Our experiments with multiple benchmarks show that Spider is effective in detecting data races in distributed executions in a practical amount of time, providing evidence of its usefulness as a testing tool. © Springer Nature Switzerland AG 2020.

Supervised
thesis

2022

Formalization of Deep Learning Techniques with the Why3 Proof Platform

Author
Márcio Alexandre Mota Sousa

Institution
UM

2022

Fiber Laser Plasma Spectroscopy for Real Time Underwater Element Analysis

Author
Miguel Fernandes Soares Ferreira

Institution
UP-FCUP

2022

Conversão para Why3 de Formalizações em Coq

Author
Bárbara Andreia Cardoso Ferreira

Institution
UM

2022

Verification of Distributed Algorithms with the Why3 tool

Author
Carla Isabel Novais da Cruz

Institution
UM

2022

Vulnerabilities preservation using code mutation

Author
Jorge Fernando Alves da Cruz

Institution
UM