Navegación

Búsqueda

Búsqueda avanzada

El autor Clara Segura ha publicado 2 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 - 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: