Static detection of pointer errors: an axiomatisation and a checking algorithm

The work

AuthorsPascal Fradet; Ronan Gaugne; Daniel Le Métayer
Editors
Typeinproceedings
Year1996
Citekeyfradet1996static

Where it appeared

Published inEuropean Symposium on Programming
PublisherSpringer
Pages125--140

Abstract

The incorrect use of pointers is one of the most common source of bugs. As a consequence, any kind of static code checking capable of detecting potential bugs at compile time is welcome. This paper presents a static analysis for the detection of incorrect accesses to memory (dereferences of invalid pointers). A pointer may be invalid because it has not been initialised or because it refers to a memory location which has been deallocated. The analyser is derived from an axiomatisation of alias and connectivity properties which is shown to be sound with respect to the natural semantics of the language. It deals with dynamically allocated data structures and it is accurate enough to handle circular structures.

A copy is held

pdf, 792.0 kB. Not published — it may be under copyright. The facts and links here are.

How it got here

How it got hereagent via bibtex
Added2026-08-05 00:00 UTC
Approved bya person 2026-08-16 15:34 UTC

Filed under

separation-logic

Cite it as

@inproceedings{fradet1996static,
  title        = {Static detection of pointer errors: an axiomatisation and a checking algorithm},
  author       = {Pascal Fradet and Ronan Gaugne and Daniel Le Métayer},
  year         = {1996},
  booktitle    = {European Symposium on Programming},
  publisher    = {Springer},
  pages        = {125--140},
  doi          = {10.1007/3-540-61055-3_33},
}

This record lives at https://refs.drheap.org/fradet1996static/ and will keep doing so.