Navegación

Búsqueda

Búsqueda avanzada

El autor Ricardo Peña ha publicado 9 artículo(s):

1 - Space Consumption Analysis by Abstract Interpretation: Reductivity Properties (High-level Work)

In a previous paper we presented an abstract interpretation-based static analysis for inferring heap and stack memory consumption in a functional language. The language, called Safe, is eager and firstorder, and its memory management system is based on heap regions instead of the more conventional approach of having a garbage collector.
In this paper we concentrate on an important property of our analysis, namely that the inferred bounds are reductive under certain reasonable conditions. This means that by iterating the analysis using as input the prior inferred bound, we can get tighter and tighter bounds, all of them correct. In some cases, even the exact bound is obtained.
The paper includes several examples and case studies illustrating in detail the reductivity property of the inferred bounds.

Autores: Manuel Montenegro  / Clara Segura / Ricardo Peña / 
Palabras Clave:

2 - An Introduction to Liquid Haskell

This paper is a tutorial introducing the underlying technology and the use of the tool Liquid Haskell, a type-checker for the functional language Haskell that can help programmers to verify non-trivial properties of their programs with a low effort.
The first sections introduce the technology of Liquid Types by explaining its principles and summarizing how its type inference algorithm manages to prove properties. The remaining sections present a selection of Haskell examples and show the kind of properties that can be proved with the
system.

Autores: Ricardo Peña / 
Palabras Clave:

3 - Synthesizing Invariants for Arrays (Work in Progress)

Liquid types can be seen as as a computer assisted verification system. Ordinary Hindley-Milner types are qualified by predicates expressing properties. In this way, the programmer may specify the preconditions and postconditions of functions. More importantly, the system infers the types of all the intermediate variables and checks that the verification conditions proving correctness hold. The predicates are currently expressed in a quantifier free decidable logic.
Here, we extend Liquid types with quantified predicates of a decidable logic for arrays, propose a concept of an array refinement type, and provide an inference algorithm for this extension. By applying this ideas to several imperative algorithms dealing with arrays, we have been able to infer
complex invariants.

Autores: Manuel Montenegro /  Susana Nieva / Ricardo Peña / Clara Segura / 
Palabras Clave:

4 - Processing an Intermediate Representation Written in Lisp

In the context of designing the verification platform CAVI-ART, we arrived to the need of deciding a textual format for our intermediate representation of programs. After considering several options, we finally decided to use S-expressions for that textual representation, and Common Lisp for processing it in order to obtain the verification conditions. In this paper, we discuss the benefits of this decision. S-expressions are homoiconic, i.e. they can be both considered as data and as code. We exploit this duality, and extensively use the facilities of the Common Lisp environment to make different processing with these textual representations. In particular, using a common compilation scheme we
show that program execution, and verification condition generation, can be seen as two instantiations of the same generic process.

Autores: Ricardo Peña /  Santiago Saavedra /  Jaime Sánchez-Hernández / 
Palabras Clave:

5 - A Tool for Black-Box Testing in a Multilanguage Verification Platform (Trabajo en progreso)

In the context of the multilanguage verification platform CAVI-ART, we have defined an Intermediate Representation (IR) to which all the source languages are translated. This IR contains both the code and the assertions given by the programmer. Its primary purpose was automatically generating and proving, in a source language independent way, the verification conditions ensuring the program correctness. The logical formulas are sent by the platform to an SMT solver which checks their validity.

In this paper we present a new use of the IR: we transform it into an executable language (that it turns out to be Haskell) and also transform the assertions into executable (Haskell) code. Thanks to that, tests can be run on the transformed program, and bugs can be detected either in the specification assertions or in the code. Moreover, we use the assertions to generate black-box test-cases from them, and also as test oracles. In this way, given the IR of a program, all the process —namely, test-case generation, test running, and test correctness checking— is completely automatic. So, thousands of tests can be run with little or none effort. The only burden for the programmer is providing the precondition and the postcondition of the code under test, which anyway should have been provided in advance, since the primary goal was to verify the program.

We discuss the problems we have encountered while implementing this idea, and how we have solved them. In particular, we report on the use of Haskell resources such as GADTs, efficient data structures, and specialized libraries.

Autores: Marta Aracil / Pedro García / Ricardo Peña / 
Palabras Clave: black box - executable assertions - Testing - verification platform

6 - Termination Analysis in a Multi-language Verification Platform (Trabajo en progreso)

One aim of the verification platform CAVI-ART is to provide as much assistance as possible to programmers in order to alleviate their verification effort. One of these aids is automatically proving termination of programs, whenever this is possible. Since CAVI-ART is a multi-language platform, the analysis is performed at the level of the platform Intermediate Representation language (IR), to which all source languages are first translated.

We have selected one of the the most successful termination tools, called RANK, and transform our IR-programs to an appropriate input for RANK. There is a fundamental mismatch between the functional, stateless, recursive flavour of our IR, and the automaton-based input of RANK, which is a tool developed for imperative, mutable-state programs. In this paper we show how we have circumvented this problem, and present an algorithm transforming the IR to an automaton. We give some examples of recursive programs that we have successfully proved terminating.

Autores: Jakub Holubanský / Álvaro Mínguez / Ricardo Peña / 
Palabras Clave: integer automata - Termination analysis - verification platform

7 - An Exercise in Proving Red-Black Trees Correct (Trabajo en progreso)

Red-black trees are an efficient data structure that constitutes the basis for implementing maps, multimaps, sets and multisets, in the standard libraries of many programming languages. It achieves logarithmic costs for searching, inserting, and deleting keys, but keeping them balanced frequently requires to deal with a high number of cases. However, a variant called «Left-Leaning», due to Robert Sedgewick, reduces the number of cases to a few ones. We present here a functional version of these red-black trees and prove them correct with respect to a model-based specification, being the model of a red-black tree a set of elements. We have used the Dafny verification platform, which provides the programming language, the assertion language, and the verifier. The latter is an up-to-date SMT solver (Satisfiability Modulo Theories), which can deal with a rather large decidable fragment of the first-order logic.

Autores: Ricardo Peña / 
Palabras Clave: Balanced Trees - Data Structures - Formal Verification - verification platforms

8 -

9 - SMT-based Test-Case Generation with Complex Preconditions

We present a system which can automatically generate an exhaustive set of black-box test-cases, up to a given size, for programs under test requiring complex preconditions. The key of the approach is to translate a formal precondition into a set of constraints belonging to the decidable logics of SMT solvers. By checking the satisfiability of the constraints, then the models returned by the solver automatically synthesize the cases.We also show how to use SMT solvers to automatically check for validity the test-case results, and also to complement the black-box cases with white-box ones. Finally, we use of solver to perform what we call automatic partial verification of the program. In summary, we propose a system in which exhaustive black-box and white-box testing, result checking, and partial verification, can all be done automatically. The only extra effort required from programmers is to write formal specifications.

Autores: Ricardo Peña / Jaime Sánchez-Hernández / Miguel Garrido / Javier Sagredo / 
Palabras Clave: formal specification - SMT solvers - test-case generation - Testing