A verified specification of TLSF memory management allocator using state monads

DOI10.1007/978-3-030-35540-1_8MaRDI QIDQ6535916zbMATH OpenFDO

Authors Yongwang Zhao, David Sanán, Lei Qiao, Jinkun Zhang

Publication date 12 March 2024

Full work available at URL https://doi.org/10.1007/978-3-030-35540-1_8

zbMATH Keywords

formal verificationIsabelle/HOLmemory management

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• A constant-time dynamic storage allocator for real-time systems
• Formal Verification of an Incremental Garbage Collector
• A TLA+ Formal Specification and Verification of a New Real-Time Communication Protocol
• Types, bytes, and separation logic
• scientific article; zbMATH DE number 1696614

Cites work

• An axiomatic specification for sequential memory models
• CompCertTSO
• Compositional verification of a baby virtual memory manager
• Formal memory models for the verification of low-level operating-system code
• Formal Pervasive Verification of a Paging Mechanism
• Formal verification of a C-like memory model and its uses for verifying program transformations
• Hierarchical shape abstraction for analysis of free list memory allocators
• scientific article; zbMATH DE number 1956565 (Why is no real title available?)
• Isabelle/HOL. A proof assistant for higher-order logic
• Model checking dynamic memory allocation in operating systems
• Secure Microkernels, State Monads and Scalable Refinement

This page was built for publication: A verified specification of TLSF memory management allocator using state monads

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