Aviso: para depositar documentos, por favor, inicia sesión e identifícate con tu cuenta de correo institucional de la UCM con el botón MI CUENTA UCM. No emplees la opción AUTENTICACIÓN CON CONTRASEÑA Disculpen las molestias.
 

Verification of mutable linear data structures and iterator-based algorithms in Dafny.

dc.contributor.authorBlázquez Saborido, Jorge
dc.contributor.authorMontenegro Montes, Manuel
dc.contributor.authorSegura Díaz, Clara María
dc.date.accessioned2023-06-22T11:16:39Z
dc.date.available2023-06-22T11:16:39Z
dc.date.issued2023-08
dc.description.abstractWe address the verification of mutable, heap-allocated abstract data types (ADTs) in Dafny, and their traversal via iterators. For this purpose, we devise a verification methodology that makes it possible to implement ADTs based on already existing ones, while maintaining proper encapsulation. Then, we apply this methodology to the specification and implementation of linear collections such as stacks, queues, deques, and lists with iterators. The approach introduced in this paper allows one to progressively refine some aspects of the specification such as iterator invalidation, so that clients of the library can reason about how structural changes to a list affect existing iterators. Finally, we extend our methodology to the verification of client code (i.e., code that makes use of the implemented ADTs) and identify the boilerplate conditions common to all methods that receive and manipulate ADTs.
dc.description.departmentDepto. de Sistemas Informáticos y Computación
dc.description.facultyFac. de Informática
dc.description.refereedTRUE
dc.description.sponsorshipMinisterio de Economía y Competitividad
dc.description.sponsorshipMinisterio de Ciencia e Innovación
dc.description.sponsorshipComunidad de Madrid
dc.description.statuspub
dc.eprint.idhttps://eprints.ucm.es/id/eprint/78283
dc.identifier.doi10.1016/j.jlamp.2023.100875
dc.identifier.issn2352-2216
dc.identifier.officialurlhttps://www.elsevier.com/locate/jlamp
dc.identifier.urihttps://hdl.handle.net/20.500.14352/72274
dc.journal.titleJournal of Logical and Algebraic Methods in Programming
dc.language.isoeng
dc.publisherElsevier
dc.relation.projectIDCAVI-ART-2 (TIN2017-86217-R)
dc.relation.projectIDProCode (PID2019-1085288RB-C22)
dc.relation.projectIDS2018/TCS-4339 (BLOQUES-CM)
dc.rightsAtribución-NoComercial-SinDerivadas 3.0 España
dc.rights.accessRightsopen access
dc.rights.urihttps://creativecommons.org/licenses/by-nc-nd/3.0/es/
dc.subject.cdu004.43
dc.subject.cdu004.89
dc.subject.keywordProgram verification
dc.subject.keywordData structures
dc.subject.keywordAbstract data types
dc.subject.keywordIterators
dc.subject.keywordDafny
dc.subject.keywordVerificación de programas
dc.subject.keywordEstructuras de datos
dc.subject.keywordTipos abstractos de datos Iteradores Dafny
dc.subject.ucmLenguajes de programación
dc.subject.ucmSoftware
dc.subject.ucmLógica simbólica y matemática (Matemáticas)
dc.subject.unesco1203.23 Lenguajes de Programación
dc.subject.unesco3304.16 Diseño Lógico
dc.subject.unesco1102.14 Lógica Simbólica
dc.titleVerification of mutable linear data structures and iterator-based algorithms in Dafny.
dc.title.alternativeVerificación de estructuras de datos lineales y algoritmos basado s en iteradores en Dafny.
dc.typejournal article
dc.volume.number134
dspace.entity.typePublication
relation.isAuthorOfPublicationdc391c7e-9682-4142-a1de-7d649b26bf3d
relation.isAuthorOfPublicationb7547876-744e-4e9b-b551-c0dfab2a2d83
relation.isAuthorOfPublication.latestForDiscoverydc391c7e-9682-4142-a1de-7d649b26bf3d

Download

Original bundle

Now showing 1 - 1 of 1
Loading...
Thumbnail Image
Name:
BlazquezMontenegroSegura.pdf
Size:
687.86 KB
Format:
Adobe Portable Document Format

Collections