Model checking dynamic memory allocation in operating systems

DOI10.1007/S10817-009-9124-YMaRDI QIDQ835783zbMATH OpenOpenAlexFDO

Authors María del Mar Gallardo, Pedro Merino, David Sanán

Publication date 31 August 2009

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s10817-009-9124-y

zbMATH Keywords

model checkingoperating systemsdynamic memory allocation

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Theory of operating systems (68N25)

Recommendations

• Extending Model Checking with Dynamic Analysis
• Abstract Regular Tree Model Checking of Complex Dynamic Data Structures
• scientific article; zbMATH DE number 910719
• Software model checking
• scientific article; zbMATH DE number 2080188

Cites work

• scientific article; zbMATH DE number 1324833 (Why is no real title available?)
• scientific article; zbMATH DE number 1956555 (Why is no real title available?)
• scientific article; zbMATH DE number 1744960 (Why is no real title available?)
• Abstract Regular Tree Model Checking of Complex Dynamic Data Structures
• First-Order and Temporal Logics for Nested Words
• Model checking JAVA programs using JAVA PathFinder
• Multi-dimensional modal logic as a framework for spatio-temporal reasoning
• Reasoning About Sequences of Memory States
• Tools and Algorithms for the Construction and Analysis of Systems
• Tools and Algorithms for the Construction and Analysis of Systems
• Tools and Algorithms for the Construction and Analysis of Systems
• Verification, Model Checking, and Abstract Interpretation

Cited in

(5)

• Verify heaps via unified model checking
• Using unified model checking to verify heaps
• The role of abstraction in model checking
• Verified runtime assertion checking for memory properties
• A verified specification of TLSF memory management allocator using state monads

Describes a project that uses

Uses Software

• dSPIN
• GROOVE
• Bandera
• Java PathFinder
• Bogor
• General Purpose Hash Function Library
• SPIN
• BLAST
• veriSoft
• jETI

This page was built for publication: Model checking dynamic memory allocation in operating systems

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