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

DOI10.1016/J.JLAMP.2023.100875MaRDI QIDQ6113015zbMATH OpenFDO

Authors Jorge Blázquez, Manuel Montenegro, Clara Segura

Publication date 8 August 2023

Published in Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)

Copyright license Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International

Full work available at URL https://doi.org/10.1016/J.JLAMP.2023.100875

zbMATH Keywords

iteratorsdata structuresprogram verificationabstract data typesDafny

Mathematics Subject Classification ID

Computer science (68-XX)

Recommendations

• Verification of finite iterations over collections of variable data structures
• Verification of a finite iteration over data structures
• Verification of finite iterations over tuples of data structures
• scientific article; zbMATH DE number 1534590
• A constructive approach for proving data structures' linearizability
• Pattern-based verification of programs with extended linear linked data structures
• Dafny: an automatic program verifier for functional correctness
• Modular verification of concurrency-aware linearizability

Cites work

• scientific article; zbMATH DE number 815103 (Why is no real title available?)
• Behavioral interface specification languages
• Correct code containing containers
• Dafny: an automatic program verifier for functional correctness
• Mechanized verification with sharing
• Modular invariants for layered object structures
• Programming Languages and Systems
• Software engineering and formal methods. 12th international conference, SEFM 2014, Grenoble, France, September 1--5, 2014. Proceedings
• Using History Invariants to Verify Observers
• Verification of mutable linear data structures and iterator-based algorithms in Dafny

Cited in

(3)

• Preface to selected papers from 20th workshop on programming and languages (PROLE 2021)
• Verification of mutable linear data structures and iterator-based algorithms in Dafny
• Polycheck: dynamic verification of iteration space transformations on affine programs

This page was built for publication: Verification of mutable linear data structures and iterator-based algorithms in Dafny

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6113015)