zbMATH — the first resource for mathematics

Shape analysis of low-level C with overlapping structures. (English) Zbl 1273.68086
Barthe, Gilles (ed.) et al., Verification, model checking, and abstract interpretation. 11th international conference, VMCAI 2010, Madrid, Spain, January 17–19, 2010. Proceedings. Berlin: Springer (ISBN 978-3-642-11318-5/pbk). Lecture Notes in Computer Science 5944, 214-230 (2010).
Summary: Device drivers often keep data in multiple data structures simultaneously while embedding list or tree related records into the records containing the actual data; this results in overlapping structures. Shape analyses have traditionally relied on a graph-based representation of memory where a node corresponds to a whole record and edges to pointers. As this is ill-suited for encoding overlapping structures, we propose and formally relate two refined memory models. We demonstrate the appropriateness of these models by implementing shape analyses based on them within the TVLA framework. The implementation is exemplified using code extracted from cache managing kernel modules.
For the entire collection see [Zbl 1178.68003].

68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68P05 Data structures
Full Text: DOI