Verifying pointer programs using separation logic and invariant based programming in Isabelle

Viorel Preoteasa*

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contributionScientificpeer-review


In this paper we present a technique based on invariant based programming and separation logic for verifying pointer programs. Invariant based programs are directed graphs where the nodes are called situations and are labeled by predicates (invariants). The edges are called transitions, and are labeled by guarded assignment statements. We represent the situations using Isabelle’s locales. A locale is a theory parameterized by constants and types. The constant parameters are used for modeling the state of the program, and the type parameters are used for obtaining generic programs. The invariants are modeled as locale assumptions (axioms), and the transitions are modeled as locale interpretations. For modeling pointer programs we use separation logic. The final result of this construction is a collection of mutually recursive Isabelle functions that implements the program. We apply this technique to Lindstrom’s algorithm for traversing a binary tree without additional memory.

Original languageEnglish
Title of host publicationIntegrated Formal Methods - 12th International Conference, IFM 2016, Proceedings
PublisherSpringer Verlag
Number of pages17
ISBN (Print)9783319336923
Publication statusPublished - 2016
MoE publication typeA4 Article in a conference publication
EventInternational Conference on Integrated Formal Methods - Reykjavik, Iceland
Duration: 1 Jun 20165 Jun 2016
Conference number: 12

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
ISSN (Print)03029743
ISSN (Electronic)16113349


ConferenceInternational Conference on Integrated Formal Methods
Abbreviated titleIFM


Dive into the research topics of 'Verifying pointer programs using separation logic and invariant based programming in Isabelle'. Together they form a unique fingerprint.

Cite this