Verification of mutable linear data structures and iterator-based algorithms in Dafny
Authors:
- Jorge BlázquezJBJorge Blázquez
- Manuel MontenegroMMManuel Montenegro
- Clara SeguraCSClara Segura
Open Access
- 5 May 2023
- journal article
- research article
- Published by Elsevier in Journal of Logical and Algebraic Methods in Programming
- Vol. 134
Abstract
No abstract availableKeywords
Funding Information
- Comunidad de Madrid
- Gobierno de España Ministerio de Ciencia e Innovación
- European Commission
- Ministerio de Economía y Competitividad (CAVI-ART-2, TIN2017-86217-R)
- Ministerio de Ciencia e Innovación (PID2019-1085288RB-C22)
- Ministerio de Economía y Competitividad
This publication has 6 references indexed in Scilit:
- A fully verified container libraryFormal Aspects of Computing, 2017
- Behavioral interface specification languagesACM Computing Surveys, 2012
- Modular invariants for layered object structuresScience of Computer Programming, 2006
- Model variables: cleanly supporting abstraction in design by contractSoftware: Practice and Experience, 2005
- Verification of Object-Oriented Programs with Invariants.The Journal of Object Technology, 2004
- A behavioral notion of subtypingACM Transactions on Programming Languages and Systems, 1994