Publication

Automatic Heap-Memory Diagrams for Separation-Logic Proofs

2026

Abstract

Separation-logic proofs of heap-manipulating programs require careful accounting of objects and pointers in memory. On paper, these proofs are often accompanied by heap-memory diagrams that help authors and readers track the evolution of the program’s abstract state. However, users of interactive theorem provers must instead work with plain-text notations that obscure object relationships. This paper presents the first automatic visualization library for separation-logic heap predicates, mimicking hand-drawn diagrams found in published materials. Four key features make the library practical. First, it supports animating across proof steps. Second, it offers users a DSL to specify how custom predicates should be visualized. Third, it is straightforward to port to new separation logic frameworks. And fourth, it can be used in browsers and IDEs, during and after proof development. We demonstrate these features by implementing support for CFML and Iris and integrating with Alectryon and VsRocq.

Official source

https://infoscience.epfl.ch/entities/publication/eeed08ac-ec99-4e2f-a7d8-afe0bfb8d3fb

About this result

This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.

Graph Chat

Chat with Graph Search

Ask any question about EPFL courses, lectures, exercises, research, news, etc. or try the example questions below.

DISCLAIMER: The Graph Chatbot is not programmed to provide explicit or categorical answers to your questions. Rather, it transforms your questions into API requests that are distributed across the various IT services officially administered by EPFL. Its purpose is solely to collect and recommend relevant references to content that you can explore to help you answer your questions.

2026

Abstract

Official source

https://infoscience.epfl.ch/entities/publication/eeed08ac-ec99-4e2f-a7d8-afe0bfb8d3fb

About this result

Related concepts (31)

Proof assistant

In computer science and mathematical logic, a proof assistant or interactive theorem prover is a software tool to assist with the development of formal proofs by human-machine collaboration. This involves some sort of interactive proof editor, or other interface, with which a human can guide the search for proofs, the details of which are stored in, and some steps provided by, a computer. A recent effort within this field is making these tools use artificial intelligence to automate the formalization of ordinary mathematics.

Isabelle (proof assistant)

The Isabelle automated theorem prover is a higher-order logic (HOL) theorem prover, written in Standard ML and Scala. As an LCF-style theorem prover, it is based on a small logical core (kernel) to increase the trustworthiness of proofs without requiring yet supporting explicit proof objects. Isabelle is available inside a flexible system framework allowing for logically safe extensions, which comprise both theories as well as implementations for code-generation, documentation, and specific support for a variety of formal methods.

Pointer (computer programming)

In computer science, a pointer is an object in many programming languages that stores a memory address. This can be that of another value located in computer memory, or in some cases, that of memory-mapped computer hardware. A pointer references a location in memory, and obtaining the value stored at that location is known as dereferencing the pointer. As an analogy, a page number in a book's index could be considered a pointer to the corresponding page; dereferencing such a pointer would be done by flipping to the page with the given page number and reading the text found on that page.