Towards Shape Analysis for Device Drivers

  • Hongseok Yang
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4349)


Shape analysis algorithms statically infer deep properties of the runtime heap, such as whether a variable points to a cyclic or acyclic linked list. Unfortunately, there are unsolved problems that make it difficult for shape analyses being to be used for real-world programs. The problems include: performance of the analysis; dealing with low-level language features; and supporting complex data-structures used in real-world programs, without sacrificing precision or performance of the analysis.

In this talk, I will present work on shape analysis for Windows device drivers based on separation logic formulae. Device drivers basically use linked lists, but complex varieties of linked list unlike those usually studied in shape analysis. I will explain the nature of those structures, which open problems matter most for our analysis, and how we approach some of those problems. In particular, I will describe how higher-order predicates let us succinctly describe a variety of data structures, and how discovery of parameters to higher-order predicates allows an analysis that is not tied to specific structures.

Copyright information

© Springer-Verlag Berlin Heidelberg 2007

Authors and Affiliations

  • Hongseok Yang
    • 1
  1. 1.Queen Mary, University of LondonUK

Personalised recommendations