Autor:
Montenegro, Manuel

Foto de perfil
E-mails conocidos
montenegro@fdi.ucm.es,
montenegro@fdi.ucm.es
Fecha de nacimiento
Proyectos de investigación
Unidades organizativas
Puesto de trabajo
Apellidos
Montenegro
Nombre de pila
Manuel
Nombre
Nombres alternativos
Afiliaciones conocidas
Departamento de sistemas Informáticos y Computación. Universidad Complutense de Madrid, Spain
Complutense University of Madrid, Spain
Universidad Complutense de Madrid
Universidad Complutense de Madrid, Spain
Páginas web conocidas
Página completa del ítem
Notificar un error en este autor

Filtros

2015 - 201922020 - 20212
Restablecer filtros

Ajustes

Resultados de la búsqueda

Mostrando 1 - 4 de 4
  • Miniatura
    Artículo
    Synthesizing Invariants for Arrays
    Montenegro, Manuel; Nieva, Susana; Peña Marí, Ricardo; Segura, Clara. Actas de las XVI Jornadas de Programación y Lenguajes (PROLE 2016), 2016-09-02.
    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.
  • Miniatura
    Artículo
    Verification of ROS Navigation using Maude
    Martin-Martin, Enrique; Montenegro, Manuel; Riesco, Adrián; Rodríguez-Hortalá, Juan; Rubio, Rubén. Actas de las XX Jornadas de Programación y Lenguajes (PROLE 2021), 2021-09-22.
    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.
  • Miniatura
    Artículo
    A Generic Intermediate Representation for Verification Condition Generation, Work in Progress
    Montenegro, Manuel; Peña Marí, Ricardo; Sánchez-Hernández, Jaime. Actas de las XV Jornadas de Programación y Lenguajes (PROLE 2015), 2015-09-15.
    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.
  • Miniatura
    Artículo
    Verification of mutable data structures in Dafny: methodological aspects
    Blázquez, Jorge; Montenegro, Manuel; Segura, Clara. Actas de las XX Jornadas de Programación y Lenguajes (PROLE 2021), 2021-09-22.
    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.