RT Conference Proceedings
T1 Verification of mutable data structures in Dafny: methodological aspects
A1 Blázquez, Jorge
A1 Montenegro Montes, Manuel
A1 Segura Díaz, Clara María
AB 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 aninstance (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.
YR 2021
FD 2021-09-22
LK https://hdl.handle.net/20.500.14352/93186
UL https://hdl.handle.net/20.500.14352/93186
LA eng
NO Ministerio de Economía y Competitividad
NO Comunidad de Madrid: S2018/TCS-4339 (BLOQUES-CM)
DS Docta Complutense
RD 7 abr 2025