Autor:
Segura, Clara

Cargando...
Foto de perfil
E-mails conocidos
csegura@sip.ucm.es
Fecha de nacimiento
Proyectos de investigación
Unidades organizativas
Puesto de trabajo
Apellidos
Segura
Nombre de pila
Clara
Nombre
Nombres alternativos
Afiliaciones conocidas
Complutense University of Madrid, Spain
Universidad Complutense de Madrid, Spain
Páginas web conocidas
Página completa del ítem
Notificar un error en este autor

Resultados de la búsqueda

Mostrando 1 - 2 de 2
  • 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.
  • 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.