zbMATH — the first resource for mathematics

Symbolic execution with separation logic. (English) Zbl 1159.68363
Yi, Kwangkeun (ed.), Programming languages and systems. Third Asian symposium, APLAS 2005, Tsukuba, Japan, November 2–5, 2005. Proceedings. Berlin: Springer (ISBN 3-540-29735-9/pbk). Lecture Notes in Computer Science 3780, 52-68 (2005).
Summary: We describe a sound method for automatically proving Hoare triples for loop-free code in Separation Logic, for certain preconditions and postconditions (symbolic heaps). The method uses a form of symbolic execution, a decidable proof theory for symbolic heaps, and extraction of frame axioms from incomplete proofs. This is a precursor to the use of the logic in automatic specification checking, program analysis, and model checking.
For the entire collection see [Zbl 1098.68007].

68N15 Theory of programming languages
PDF BibTeX Cite
Full Text: DOI