2026-06-08T12:40:18Zhttps://docta.ucm.es/rest/oai/request

oai:docta.ucm.es:20.500.14352/931862025-03-18T13:28:31Zcom_20.500.14352_14col_20.500.14352_15

Verification of mutable data structures in Dafny: methodological aspects Blázquez, Jorge Montenegro Montes, Manuel Segura Díaz, Clara María Lenguajes de programación 1203.23 Lenguajes de Programación 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. Ministerio de Economía y Competitividad Comunidad de Madrid: S2018/TCS-4339 (BLOQUES-CM) Depto. de Sistemas Informáticos y Computación Fac. de Informática TRUE pub 2024-01-15T16:46:08Z 2024-01-15T16:46:08Z 2021-09-22 conference paper AM https://hdl.handle.net/20.500.14352/93186 XXXX-XXXX eng info:eu-repo/grantAgreement/AEI/Plan Estatal de Investigación Científica y Técnica y de Innovación 2013-2016/TIN2017-86217-R/ES/CAVI-ART-2: VALIDACION ASISTIDA DE PROGRAMAS MEDIANTE ANALISIS, ANOTACIONES, DEMOSTRACIONES MATEMATICAS Y PRUEBAS DE EJECUCION/ Attribution-NonCommercial-NoDerivatives 4.0 International http://creativecommons.org/licenses/by-nc-nd/4.0/ open access application/pdf