A verified specification of TLSF memory management allocator using state monads
From MaRDI portal
Publication:6535916
DOI10.1007/978-3-030-35540-1_8zbMath1543.68238MaRDI QIDQ6535916
Jinkun Zhang, Yongwang Zhao, Unnamed Author, Lei Qiao, David Sanán
Publication date: 12 March 2024
Cites Work
- Unnamed Item
- Formal memory models for the verification of low-level operating-system code
- Model checking dynamic memory allocation in operating systems
- Formal verification of a C-like memory model and its uses for verifying program transformations
- Isabelle/HOL. A proof assistant for higher-order logic
- An axiomatic specification for sequential memory models
- Hierarchical shape abstraction for analysis of free list memory allocators
- Secure Microkernels, State Monads and Scalable Refinement
- Compositional Verification of a Baby Virtual Memory Manager
- CompCertTSO
- Formal Pervasive Verification of a Paging Mechanism
This page was built for publication: A verified specification of TLSF memory management allocator using state monads
