TY  - JOUR
AU  - Blázquez Saborido, Jorge
AU  - Montenegro Montes, Manuel
AU  - Segura Díaz, Clara María
PY  - 2023
DO  - 10.1016/j.jlamp.2023.100875
SN  - 2352-2216
UR  - https://hdl.handle.net/20.500.14352/72274
T2  - Journal of Logical and Algebraic Methods in Programming
AB  - 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...
LA  - eng
PB  - Elsevier
KW  - Program verification
KW  - Data structures
KW  - Abstract data types
KW  - Iterators
KW  - Dafny
KW  - Verificación de programas
KW  - Estructuras de datos
KW  - Tipos abstractos de datosIteradoresDafny
TI  - Verification of mutable linear data structures and iterator-based algorithms in Dafny.
T2  - Verificación de estructuras de datos lineales y algoritmos basado s en iteradores en Dafny.
TY  - journal article
VL  - 134
ER  -