Cookies
O website necessita de alguns cookies e outros recursos semelhantes para funcionar. Caso o permita, o INESC TEC irá utilizar cookies para recolher dados sobre as suas visitas, contribuindo, assim, para estatísticas agregadas que permitem melhorar o nosso serviço. 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

2020

Real-time MTL with durations as SMT with applications to schedulability analysis

Autores
de Matos, A; Leucker, M; Pereira, D; Pinto, JS;

Publicação
2020 INTERNATIONAL SYMPOSIUM ON THEORETICAL ASPECTS OF SOFTWARE ENGINEERING (TASE 2020)

Abstract
This paper introduces a synthesis procedure for the satisfiability problem of RMTL-integral formulas as SAT solving modulo theories. RMTL-integral is a real-time version of metric temporal logic (MTL) extended by a duration quantifier allowing to measure time durations. For any given formula, a SAT instance modulo the theory of arrays, uninterpreted functions with equality and non-linear real-arithmetic is synthesized and may then be further investigated using appropriate SMT solvers. We show the benefits of using RMTL-integral with the given SMT encoding on a diversified set of examples that include in particular its application in the area of schedulability analysis. Therefore, we introduce a simple language for formalizing schedulability problems and show how to formulate timing constraints as RMTL-integral formulas. Our practical evaluation based on our synthesis and Z3 as back-end SMT solver also shows the feasibility of the overall approach.

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

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

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

2018

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

Autor
André de Matos Pedro

Instituição
UM