Búsqueda avanzada

El autor Manuel Montenegro ha publicado 7 artículo(s):

1 - A Generic Intermediate Representation for Verification Condition Generation, Work in Progress

As part of a platform for computer-assisted verification, we present an intermediate representation of programs that is both language independent and appropriate for the generation of verification conditions. We show how many imperative and functional languages can be translated to this generic internal representation, and how the generated conditions faithfully reflect the semantics of the original program. At this representation level, loop invariants and preconditions of recursive functions belonging to the original program are represented by assertions placed at certain edges of a directed graph. The paper defines the generic representation, sketches the transformation algorithms, and describes how the places where the invariants should be placed are computed. Assuming that, either manually or assisted by the platform, the invariants have been settled, it is shown how the verification conditions are generated. A running example illustrates the process.

Autores: Manuel Montenegro /  Ricardo Peña / Jaime Sánchez-Hernández / 
Palabras Clave: intermediate representation - program transformation. - verification conditions - verification platforms

2 - 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:

3 - Polymorphic Types in Erlang Function Specifications

Erlang is a concurrent functional programming language developed by Ericsson, well suited for implementing distributed systems. Although Erlang is dynamically typed, the Dialyzer static analysis tool can be used to extract implicit type information from the programs, both for documentation
purposes and for finding errors that will definitively arise at program execution. Dialyzer is based on the notion of success types, that correspond to safe over-approximations for the semantics of expressions. Erlang also supports user given function specifications (or just specs), that are contracts
providing more information about the semantics of functions. Function specs are useful not only as documentation, but also can be employed by Dialyzer to improve the precision of the analysis. Even though specs can have a polymorphic shape, in practice Dialyzer is not able to exploit all their potential. One reason for that is that extending the notion of success type to a polymorphic setting is not trivial, and several interpretations are possible. In this work [1] we propose a precise formulation for a novel interpretation of function specs as polymorphic success types, and a program transformation that allows us to apply this new interpretation on the call sites of functions with a declared spec. This results on a significant improvement in the number of definite errors that Dialyzer is able to detect.

Autores: Francisco Javier López-Fraguas, / Manuel Montenegro / Juan Rodríguez-Hortalá / 
Palabras Clave:

4 - 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:

5 - A type derivation system for Erlang (Trabajo en progreso)

Erlang is a dynamically typed concurrent functional language of increasing interest in industry and academy. Official Erlang distributions come equipped with Dialyzer, a useful static analysis tool able to anticipate runtime errors by inferring so-called success types, which are overapproximations to the real semantics of expressions. However, Dialyzer exhibits two main weaknesses: on the practical side, its ability to deal with functions that are typically polymorphic is rather poor; and on the theoretical side, a fully developed theory for its underlying type system –comparable to, say, Hindley-Milner system– does not seem to exist, something that we consider a regrettable circumstance. This work in progress is the starting point of a medium-term project aiming at improving both aspects, so that at its end we should have proposed a full type system able to infer polymorphic success types for Erlang programs, accompanied by solid theoretical foundations including adequateness results for the type system. In this first step we only provide a derivation system of monomorphic success types for Erlang, along with correctness results with respect to a suitable semantics for the language.

Autores: Francisco Javier López-Fraguas / Manuel Montenegro / Gorka Suárez-García / 
Palabras Clave: Dialyzer - Erlang - program semantics - Success types - Type Systems

6 - Verification of ROS Navigation using Maude

The Robot Operating System (ROS) is a framework for building robust software for complex robot systems in several domains. The emph{Navigation Stack} stands out among the different libraries available in ROS. This library provides a set of reusable components that developers can use to build robots with autonomous navigation capabilities. This is a critical component, as navigation failures could have catastrophical consequences for applications like self-driving cars.Here we show our work on the verification of the C++ code for the navfn planner, which is the main planner component of the Navigation Stack. We have ported the planner to a Maude specification, and validated their equivalence using differential testing techniques. For this purpose, we integrated the specification into ROS using a novel high performance Python interface for Maude. We then analyzed the Maude specification by means of model checking and functional verification techniques, using not only the built-in tools of Maude, but also a translation into Dafny, and a manual but systematic generation of verification conditions from the Maude specification. Along the way we also encountered counterexamples for some soundness properties —e.g. that paths should not collide with obstacles— and optimatility —paths should have the lowest possible cost— of the NavFn planner.

Autores: Enrique Martin-Martin / Manuel Montenegro / Adrián Riesco / Juan Rodríguez-Hortalá / Rubén Rubio / 
Palabras Clave: Dafny - Formal Verification - Maude - Model checking - Navigation - Rewriting Logic - ROS

7 - Verification of mutable data structures in Dafny: methodological aspects

We address the verification of mutable, heap-allocated abstract data types (ADTs) in Dafny. In particular, we devise a generic verification methodology and apply it to the specification and implementation of linear collections such as stacks, queues, deques, and lists with iterators. The layered approach presented in this paper allows us to progressively refine some aspects of the specification, such as iterator invalidation. We also introduce a stratified view of the footprint of an instance (i.e. the set of memory locations owned by that instance), and identify the boilerplate conditions common to all operations of an ADT. We also show the usage of the resulting implementations by means of verified examples.

Autores: Jorge Blázquez / Manuel Montenegro / Clara Segura / 
Palabras Clave: abstract data types - Dafny - Data Structures - program verification