Specifying and verifying higher-order Rust iterators

DOI10.1007/978-3-031-30820-8_9zbMATH Open1547.68077MaRDI QIDQ6536125

Xavier Denis, Jacques-Henri Jourdan

Publication date: 5 April 2024

zbMATH Keywords

iteratorsclosuresdeductive verificationRust

Mathematics Subject Classification ID

Theory of programming languages (68N15) Specification and verification (program logics, model checking, etc.) (68Q60)

Cites Work

• Viper: A Verification Infrastructure for Permission-Based Reasoning
• A Hoare Logic for Call-by-Value Functional Programs
• RustHorn: CHC-Based Verification for Rust Programs
• Characteristic formulae for the verification of imperative programs

This page was built for publication: Specifying and verifying higher-order Rust iterators

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