Cookies Policy
We use cookies to improve our site and your experience. By continuing to browse our site you accept our cookie policy. Find out More
Close
  • Menu
About

About

I am an Assistant Professor at the Department of Informatics of the University of Minho and a researcher at HASLab/INESC TEC. I obtained is PhD degree in Computer Science from this university in 2004. My research interests include formal methods, program verification, type systems and logic.

Interest
Topics
Details

Details

  • Name

    Maria João Frade
  • Cluster

    Computer Science
  • Role

    Senior Researcher
  • Since

    01st November 2011
001
Publications

2018

A Generalized Approach to Verification Condition Generation

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

Publication
2018 IEEE 42nd Annual Computer Software and Applications Conference, COMPSAC 2018, Tokyo, Japan, 23-27 July 2018, Volume 1

Abstract

2018

A Generalized Approach to Verification Condition Generation

Authors
Belo Lourenco, C; Frade, MJ; Nakajima, S; Sousa Pinto, J;

Publication
Proceedings - International Computer Software and Applications Conference

Abstract
In a world where many human lives depend on the correct behavior of software systems, program verification assumes a crucial role. Many verification tools rely on an algorithm that generates verification conditions (VCs) from code annotated with properties to be checked. In this paper, we revisit two major methods that are widely used to produce VCs: predicate transformers (used mostly by deductive verification tools) and the conditional normal form transformation (used in bounded model checking of software). We identify three different aspects in which the methods differ (logical encoding of control flow, use of contexts, and semantics of asserts), and show that, since they are orthogonal, they can be freely combined. This results in six new hybrid verification condition generators (VCGens), which together with the fundamental methods constitute what we call the VCGen cube. We consider two optimizations implemented in major program verification tools and show that each of them can in fact be applied to an entire face of the cube, resulting in optimized versions of the six hybrid VCGens. Finally, we compare all VCGens empirically using a number of benchmarks. Although the results do not indicate absolute superiority of any given method, they do allow us to identify interesting patterns. © 2018 IEEE.

2018

Permutability in proof terms for intuitionistic sequent calculus with cuts

Authors
Santo, JE; Frade, MJ; Pinto, L;

Publication
Leibniz International Proceedings in Informatics, LIPIcs

Abstract
This paper gives a comprehensive and coherent view on permutability in the intuitionistic sequent calculus with cuts. Specifically we show that, once permutability is packaged into appropriate global reduction procedures, it organizes the internal structure of the system and determines fragments with computational interest, both for the computation-as-proof-normalization and the computation-as-proof-search paradigms. The vehicle of the study is a ?-calculus of multiary proof terms with generalized application, previously developed by the authors (the paper argues this system represents the simplest fragment of ordinary sequent calculus that does not fall into mere natural deduction). We start by adapting to our setting the concept of normal proof, developed by Mints, Dyckhoff, and Pinto, and by defining natural proofs, so that a proof is normal iff it is natural and cut-free. Natural proofs form a subsystem with a transparent Curry- Howard interpretation (a kind of formal vector notation for -terms with vectors consisting of lists of lists of arguments), while searching for normal proofs corresponds to a slight relaxation of focusing (in the sense of LJT). Next, we define a process of permutative conversion to natural form, and show that its combination with cut elimination gives a concept of normalization for the sequent calculus. We derive a systematic picture of the full system comprehending a rich set of reduction procedures (cut elimination, flattening, permutative conversion, normalization, focalization), organizing the relevant subsystems and the important subclasses of cut-free, normal, and focused proofs. © José Espírito Santo, Maria João Frade, and Luís Pinto; licensed under Creative Commons License CC-BY 22nd International Conference on Types for Proofs and Programs (TYPES 2016).

2016

Formalizing single-assignment program verification: An adaptation-complete approach

Authors
Lourenco, CB; Frade, MJ; Pinto, JS;

Publication
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

Abstract
Deductive verification tools typically rely on the conversion of code to a single-assignment (SA) form. In this paper we formalize program verification based on the translation of While programs annotated with loop invariants into a dynamic single-assignment language with a dedicated iterating construct, and the subsequent generation of compact, indeed linear-size, verification conditions. Soundness and completeness proofs are given for the entire workflow, including the translation of annotated programs to SA form. The formalization is based on a program logic that we show to be adaptation-complete. Although this important property has not, as far as we know, been established for any existing program verification tool, we believe that adaptationcompleteness is one of the major motivations for the use of SA form as an intermediate language. Our results here show that indeed this allows for the tools to achieve the maximum degree of adaptation when handling subprograms. © Springer-Verlag Berlin Heidelberg 2016.

2014

A Bounded Model Checker for SPARK Programs

Authors
Lourenco, CB; Frade, MJ; Pinto, JS;

Publication
AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS, ATVA 2014

Abstract
This paper discusses the design and implementation of a bounded model checker for SPARK code, and provides a proof of concept of the utility and practicality of bounded verification for SPARK.

Supervised
thesis

2016

Correct Translation of Imperative Programs to Single Assignment Form

Author
Marta Vasconcelos Castro Azevedo

Institution
UM

2015

AuTGen-C: uma plataforma para geração de testes com base no CBMC

Author
Fábio Esteves Sousa

Institution
UM