Model checking dynamic memory allocation in operating systems

DOI10.1007/s10817-009-9124-yzbMath1192.68147OpenAlexW2045662659MaRDI QIDQ835783

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)

Related Items (3)

Using Unified Model Checking to Verify Heaps ⋮ The role of abstraction in model checking ⋮ Verify heaps via unified model checking

Uses Software

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

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Model checking JAVA programs using JAVA PathFinder
• Multi-dimensional modal logic as a framework for spatio-temporal reasoning
• Abstract Regular Tree Model Checking of Complex Dynamic Data Structures
• First-Order and Temporal Logics for Nested Words
• Tools and Algorithms for the Construction and Analysis of Systems
• Reasoning About Sequences of Memory States
• Tools and Algorithms for the Construction and Analysis of Systems
• Verification, Model Checking, and Abstract Interpretation
• Tools and Algorithms for the Construction and Analysis of Systems

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