Cookies
Usamos cookies para melhorar nosso site e a sua experiência. Ao continuar a navegar no site, você aceita a nossa política de cookies. Ver mais
Aceitar Rejeitar
  • Menu
Tópicos
de interesse
Detalhes

Detalhes

  • Nome

    Jorge Sousa Pinto
  • Cluster

    Informática
  • Cargo

    Investigador Coordenador
  • Desde

    01 novembro 2011
001
Publicações

2021

A deductive reasoning approach for database applications using verification conditions

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

Publicação
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

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

Publicação
Tests and Proofs - Lecture Notes in Computer Science

Abstract

2019

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

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

Publicação
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.

2018

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

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

Publicação
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-?

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

Publicação
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

Teses
supervisionadas

2020

Scalable Trace Analysis of Distributed Systems Finding data races

Autor
João Carlos Mendes Pereira

Instituição
UM

2019

Early Validation of System Requirements and Design

Autor
Marcelo António Caridade Miranda

Instituição
UM

2018

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

Autor
André de Matos Pedro

Instituição
UM

2018

Single-assignment Program Verification

Autor
Cláudio Filipe Belo da Silva Lourenço

Instituição
UM

2018

Verificação Funcional de Controladores Arduino

Autor
Rafael Alexandre Antunes Barbosa

Instituição
UM