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
    Publications

    Publications by Jorge Sousa Pinto

    2009

    Deductive Verification of Cryptographic Software

    Authors
    Barbosa, M; Almeida, JB; Pinto, JS; Vieira, B;

    Publication
    First NASA Formal Methods Symposium - NFM 2009, Moffett Field, California, USA, April 6-8, 2009.

    Abstract

    2010

    A Deductive Verification Platform for Cryptographic Software

    Authors
    Barbosa, M; Pinto, JS; Filliâtre, JC; Vieira, B;

    Publication
    ECEASST

    Abstract

    2010

    GamaSlicer: An online laboratory for program verification and analysis

    Authors
    Da Cruz, D; Henriques, PR; Pinto, JS;

    Publication
    Proceedings of the 10th Workshop on Language Descriptions, Tools and Applications, LDTA 2010

    Abstract
    In this paper we present the GamaSlicer tool, which is primarily a semantics-based program slicer that also offers formal verification (generation of verification conditions) and program visualization functionality. The tool allows users to obtain slices using a number of different families of slicing algorithms (precondition-based, postcondition-based, and specification-based), from a correct software component annotated with pre and postconditions (contracts written in JML-annotated Java). Each family in turn contains algorithms of different precision (with more precise algorithms being asymptotically slower). A novelty of our work at the theoretical level is the inclusion of a new, much more effective algorithm for specification-based slicing, and in fact other current work at this level is being progressively incorporated in the tool. The tool also generates (in a step-by-step fashion) a set of verification conditions (as formulas written in the SMT-lib language, which enables the use of different automatic SMT provers). This allows to establish the initial correctness of the code with respect to their contracts. © ACM 2010.

    CloseRead Abstract

    2009

    Language Engineering and Rigorous Software Development, International LerNet ALFA Summer School 2008, Piriapolis, Uruguay, February 24 - March 1, 2008, Revised Tutorial Lectures

    Authors
    Bove, A; Barbosa, LS; Pardo, A; Pinto, JS;

    Publication
    LerNet ALFA Summer School

    Abstract

    2016

    A Single-Assignment Translation for Annotated Programs

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

    Publication
    CoRR

    Abstract

    2024

    Exploring Frama-C Resources by Verifying Space Software

    Authors
    Busquim e Silva, RA; Arai, NN; Burgareli, LA; Parente de Oliveira, JM; Sousa Pinto, J;

    Publication
    Computer Science Foundations and Applied Logic

    Abstract

    • 11
    • 11