Verification of mutable linear data structures and iterator-based algorithms in Dafny.
dc.contributor.author | Blázquez Saborido, Jorge | |
dc.contributor.author | Montenegro Montes, Manuel | |
dc.contributor.author | Segura Díaz, Clara María | |
dc.date.accessioned | 2023-06-22T11:16:39Z | |
dc.date.available | 2023-06-22T11:16:39Z | |
dc.date.issued | 2023-08 | |
dc.description.abstract | We 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.department | Depto. de Sistemas Informáticos y Computación | |
dc.description.faculty | Fac. de Informática | |
dc.description.refereed | TRUE | |
dc.description.sponsorship | Ministerio de Economía y Competitividad | |
dc.description.sponsorship | Ministerio de Ciencia e Innovación | |
dc.description.sponsorship | Comunidad de Madrid | |
dc.description.status | pub | |
dc.eprint.id | https://eprints.ucm.es/id/eprint/78283 | |
dc.identifier.doi | 10.1016/j.jlamp.2023.100875 | |
dc.identifier.issn | 2352-2216 | |
dc.identifier.officialurl | https://www.elsevier.com/locate/jlamp | |
dc.identifier.uri | https://hdl.handle.net/20.500.14352/72274 | |
dc.journal.title | Journal of Logical and Algebraic Methods in Programming | |
dc.language.iso | eng | |
dc.publisher | Elsevier | |
dc.relation.projectID | CAVI-ART-2 (TIN2017-86217-R) | |
dc.relation.projectID | ProCode (PID2019-1085288RB-C22) | |
dc.relation.projectID | S2018/TCS-4339 (BLOQUES-CM) | |
dc.rights | Atribución-NoComercial-SinDerivadas 3.0 España | |
dc.rights.accessRights | open access | |
dc.rights.uri | https://creativecommons.org/licenses/by-nc-nd/3.0/es/ | |
dc.subject.cdu | 004.43 | |
dc.subject.cdu | 004.89 | |
dc.subject.keyword | Program verification | |
dc.subject.keyword | Data structures | |
dc.subject.keyword | Abstract data types | |
dc.subject.keyword | Iterators | |
dc.subject.keyword | Dafny | |
dc.subject.keyword | Verificación de programas | |
dc.subject.keyword | Estructuras de datos | |
dc.subject.keyword | Tipos abstractos de datos Iteradores Dafny | |
dc.subject.ucm | Lenguajes de programación | |
dc.subject.ucm | Software | |
dc.subject.ucm | Lógica simbólica y matemática (Matemáticas) | |
dc.subject.unesco | 1203.23 Lenguajes de Programación | |
dc.subject.unesco | 3304.16 Diseño Lógico | |
dc.subject.unesco | 1102.14 Lógica Simbólica | |
dc.title | Verification of mutable linear data structures and iterator-based algorithms in Dafny. | |
dc.title.alternative | Verificación de estructuras de datos lineales y algoritmos basado s en iteradores en Dafny. | |
dc.type | journal article | |
dc.volume.number | 134 | |
dspace.entity.type | Publication | |
relation.isAuthorOfPublication | dc391c7e-9682-4142-a1de-7d649b26bf3d | |
relation.isAuthorOfPublication | b7547876-744e-4e9b-b551-c0dfab2a2d83 | |
relation.isAuthorOfPublication.latestForDiscovery | dc391c7e-9682-4142-a1de-7d649b26bf3d |
Download
Original bundle
1 - 1 of 1
Loading...
- Name:
- BlazquezMontenegroSegura.pdf
- Size:
- 687.86 KB
- Format:
- Adobe Portable Document Format