Autor:
Blázquez, Jorge

Cargando...
Foto de perfil

E-mails conocidos

jorblazq@ucm.es

Fecha de nacimiento

Proyectos de investigación

Unidades organizativas

Puesto de trabajo

Apellidos

Blázquez

Nombre de pila

Jorge

Nombre

Nombres alternativos

Afiliaciones conocidas

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