Detail publikace

Byte-Precise Verification of Low-Level List Manipulation

Originální název

Byte-Precise Verification of Low-Level List Manipulation

Anglický název

Byte-Precise Verification of Low-Level List Manipulation

Jazyk

en

Originální abstrakt

We propose a new approach to shape analysis of programs with linked lists that use low-level memory operations. Such operations include pointer arithmetic, safe usage of invalid pointers, block operations with memory, reinterpretation of the memory contents, address alignment, etc. Our approach is based on a new representation of sets of heaps, which is to some degree inspired by works on separation logic with higher-order list predicates, but it is graph-based and uses a more fine-grained (byte-precise) memory model in order to support the various low-level memory operations. The approach was implemented in the Predator tool and successfully validated on multiple non-trivial case studies that are beyond the capabilities of other current fully automated shape analysis tools.

Anglický abstrakt

We propose a new approach to shape analysis of programs with linked lists that use low-level memory operations. Such operations include pointer arithmetic, safe usage of invalid pointers, block operations with memory, reinterpretation of the memory contents, address alignment, etc. Our approach is based on a new representation of sets of heaps, which is to some degree inspired by works on separation logic with higher-order list predicates, but it is graph-based and uses a more fine-grained (byte-precise) memory model in order to support the various low-level memory operations. The approach was implemented in the Predator tool and successfully validated on multiple non-trivial case studies that are beyond the capabilities of other current fully automated shape analysis tools.

BibTex


@inproceedings{BUT103494,
  author="Kamil {Dudka} and Petr {Peringer} and Tomáš {Vojnar}",
  title="Byte-Precise Verification of Low-Level List Manipulation",
  annote="We propose a new approach to shape analysis of programs with linked lists that
use low-level memory operations. Such operations include pointer arithmetic, safe
usage of invalid pointers, block operations with memory, reinterpretation of the
memory contents, address alignment, etc. Our approach is based on a new
representation of sets of heaps, which is to some degree inspired by works on
separation logic with higher-order list predicates, but it is graph-based and
uses a more fine-grained (byte-precise) memory model in order to support the
various low-level memory operations. The approach was implemented in the Predator
tool and successfully validated on multiple non-trivial case studies that are
beyond the capabilities of other current fully automated shape analysis tools.",
  address="Springer Verlag",
  booktitle="20th Static Analysis Symposium",
  chapter="103494",
  edition="Lecture Notes in Computer Science Volume 7935",
  howpublished="print",
  institution="Springer Verlag",
  number="7935",
  year="2013",
  month="may",
  pages="215--237",
  publisher="Springer Verlag",
  type="conference paper"
}