# Combining Deductive Verification with Shape Analysis

Téo Bernier, Yani Ziani, Nikolai Kosmatov, Frédéric Loulergue

► To cite this version:

Téo Bernier, Yani Ziani, Nikolai Kosmatov, Frédéric Loulergue. Combining Deductive Verification with Shape Analysis. 27th International Conference on Fundamental Approaches to Software Engineering (FASE), 2024, Luxembourg, Luxembourg. pp.280-289, 10.1007/978-3-031-57259-3_14. hal-04354615

HAL Id: hal-04354615

https://hal.science/hal-04354615v1

Submitted on 20 Nov 2025

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
PREPRINT*
Combining Deductive Verification
with Shape Analysis

Téo Bernier¹ Yani Ziani¹,² Nikolai Kosmatov¹ Frédéric Loulergue²

¹ Thales Research & Technology, Palaiseau, France
{teo.bernier,yani.ziani,nikolai.kosmatov}@thalesgroup.com

² Université d'Orléans, INSA Centre Val de Loire, LIFO UR 4022, Orléans, France
frederic.loulergue@univ-orleans.fr

**Abstract**

Deductive verification tools can prove a large range of program properties, but often face issues on recursive data structures. Abstract interpretation tools based on separation logic and shape analysis can efficiently reason about such structures but cannot deal with so large classes of properties. This short paper presents an ongoing work on combining both techniques. We show how a deductive verifier for C programs, FRAMA-C/WP, can benefit from a shape analysis tool, MEMCAD, where structural and separation properties proved in the latter become assumptions for the former. A case study on selected functions of the TPM2-TSS library using linked lists confirms the interest of the approach.

**Keywords:** deductive verification, shape analysis, abstract interpretation, linked lists, Frama-C, MEMCAD

# 1 Introduction

**Context and Motivation.** Deductive verification tools were successfully used in many case studies [4] to prove a large range of safety, security and functional properties. Such tools often have issues to conduct automatic proof on code with recursive data structures (e.g. linked lists, trees, etc.), in particular, due to complex memory models they need. The user has to guide the proof by interactively proved lemmas, assertions, etc. Abstract interpretation tools based on separation logic and shape analysis [3] can efficiently reason about such structures but typically cannot deal with so large classes of properties. This short paper presents new ideas and emerging results on combining both techniques trying to take the best of both worlds.

**Approach and Results.** We present a verification approach combining a popular deductive verifier for C programs, FRAMA-C/WP [6], with a shape analysis tool, MEMCAD [10]. The main idea is to prove structural and separation properties in MEMCAD and then to assume them in FRAMA-C/WP in order to increase the level of automation of the latter and overcome some of its limitations. We apply it on a real-life case study using linked lists: a few (slightly simplified) functions

<footnote>*Final paper published in the proceedings of the International Conference on Fundamental Approaches to Software Engineering, doi: 10.1007/978-3-031-57259-3_14</footnote>
of tpm2-tss<fnref n="1" />, a popular library for communication with a Trusted Platform Module (TPM). Recent work [11] demonstrated that deductive verification of the library functions manipulating linked lists was relatively hard, and required many additional lemmas and assertions.

The contributions of this paper include the presentation of a combined verification technique using deductive verification and shape analysis, its illustration with FRAMA-C/WP and MEMCAD on a function manipulating linked lists, as well as a successful case study on a set of functions of the tpm2-tss library.

# 2 Background

## 2.1 Deductive Verification with Frama-C/Wp

FRAMA-C [6] is an integrated toolbox built around a kernel offering core services and plugins dedicated to specific analysis or verification tasks for C code, e.g. value analysis, runtime assertion checking and deductive verification. ACSL (ANSI C Specification Language) [6] is the common specification language of the plugins. The WP plugin performs modular deductive verification: each function is verified independently. It generates verification conditions (VCs) from the C code with ACSL annotations and requests their proof by the QED simplifier or by external provers.

We illustrate the main ACSL features on the running example<fnref n="2" /> of Fig. 1, 3, 4, 5, presented as we go, where ACSL notation (e.g. \forall, integer, ===> , < = , & & ) is pretty-printed (resp., as ∀ , Z , ⇒ , ≤ , ∧ ). Lines 69–85 of Fig. 4 show a contract for function list_push (detailed below) that adds a new value into a linked list (cf. Lines 1–2 of Fig. 1), allocating a new cell. The contract includes pre-conditions ( requires clauses) and post-conditions ( ensures clauses). The assigns clause is a special kind of post-condition that indicates the memory locations the function is allowed to modify. ACSL formulas are mostly multi-sorted first-order logic where types are either C types or logic types (such as Z , the type of mathematical integers). ACSL provides built-in constructs such as \result (the value returned by the function) and predicates such as \valid( p ) (stating that pointer p refers to an allocated memory location, so that * p can be safely read and written) and \separated( p 1,p 2,...) (stating that the memory locations referred to by given pointers do not intersect). Notice that the considered memory locations are here indicated by pointers. Users can define predicates such as those in Fig. 1, adapted here from a previous work [1] on verifying linked lists in WP.

The main predicate is the inductively defined predicate linked_11 (Lines 10–19) stating that a linked list (segment) of int values (defined on Lines 1–2) from pointer bl to pointer el (excluded) is a well-formed list represented by an ACSL logical list 11. In other words, 11 contains the pointers to the cells of that list segment (or the whole list if el is NULL ). ACSL lists are similar to lists in functional programming. In the inductive case ( linked_11_cons ) overlapping list cells (or cyclic lists) are avoided by requiring that the first cell bl is separated from all the other cells in the list including el , so the list is well-formed. The predicates on Lines 4–9 use predefined functions: \length and \nth that returns the n th element of a logic list. Predicates can take one or several program points (C labels plus some ACSL labels: Pre and Post ). The built-in \at(e, L) specifies the value of an expression e at a label L . Using these features, unchanged_11 states that a logic list does not change between two program points (Lines 20–24). Finally, Lines 25–36 define an axiomatic function to_11 that constructs a logic list from a C linked list. While it would be possible to write requires ∃ \list<cell> 11; linked_11 (*p 1, NULL , 11) ; instead of Line 72 of Figure 4, the scope of the existential quantifier is just this line. Therefore, 11 cannot be used in the post-conditions, hence the need for to_11 .

Let us now detail the contract of list_push (its code is detailed below). The pre-conditions state

<footnote n="1">¹https://github.com/tpm2-software/tpm2-tss</footnote>

<footnote n="2">²Available in a companion artifact on http://doi.org/10.5281/zenodo.10497923</footnote>
```c
1 typedef struct cell_s {struct cell_s* next; int data;} cell;
2 typedef cell* list;
3 /*@
4 predicate ptr_sep_from_list{L}(cell* c, \list<cell*> ll) =
5     ∀ Z n; 0 ≤ n < \length(ll) ⇒ \separated(c, \nth(ll, n));
6 predicate dptr_sep_from_list{L}(cell** c, \list<cell*> ll) =
7     ∀ Z n; 0 ≤ n < \length(ll) ⇒ \separated(c, \nth(ll, n));
8 predicate in_list{L}(cell* c, \list<cell*> ll) =
9     ∃ Z n; 0 ≤ n < \length(ll) ∧ \nth(ll, n) == c;
10 inductive linked LL{L}(cell *bl, cell *el, \list<cell*> ll) {
11     case linked llNil{L}:
12         ∀ cell *el; linked ll{L}(el, el, \Nil);
13     case linked llCons{L}:
14         ∀ cell *bl, *el, \list<cell*> tail;
15         (\separated(bl, el) ∧ \valid(bl) ∧
16          linked ll{L}(bl->next, el, tail) ∧
17          ptr_sep_from_list(bl, tail)) ⇒
18          linked ll{L}(bl, el, \Cons(bl, tail));
19     }
20 predicate unchanged ll{L1, L2}(\list<cell*> ll) =
21     ∀ Z n; 0 ≤ n < \length(ll) ⇒
22     \valid{L1}(\nth(ll, n)) ∧ \valid{L2}(\nth(ll, n)) ∧
23     \at((\nth(ll, n)) -> next, L1) == \at((\nth(ll, n)) -> next, L2) ∧
24     \at((\nth(ll, n)) -> data, L1) == \at((\nth(ll, n)) -> data, L2);
25 axiomatic cell_to LL {
26     logic \list<cell*> to ll{L}(cell* beg, cell* end)
27     reads {node->next | cell* node;
28         \valid(node) ∧ in_list(node, to ll(beg, end))};
29 axiom to llNil{L}: ∀ cell *node;
30     to ll{L}(node, node) == \Nil;
31 axiom to llCons{L}: ∀ cell *beg, *end;
32     (\separated(beg, end) ∧ \valid{L}(beg) ∧
33      ptr_sep_from_list{L}(beg, to ll{L}(beg->next, end)) ⇒
34      to ll{L}(beg, end) ==
35      \Cons(beg, to ll{L}(beg->next, end));
36 }
37 */
38 #include "lemmas_min.h"
```

<caption>Figure 1: Types and ACSL predicates for linked lists.</caption>

that `pl` is a valid pointer to a list (Line 70), separated from every element in the list (Line 71), and refers to a linked list verifying the inductive predicate `linked ll` (Line 72). Line 73 specifies that the only locations the function is allowed to modify are `*pl`, the head pointer of the list, and `\at(**pl, Post)`, the first element of the list at the exit point, i.e. the freshly allocated cell. We cannot reference the new list cell at the entry point because it is not allocated yet. In post-conditions, the returned value indicates whether or not the allocation is successful (Line 76). Regardless of the success, we expect the list invariants to hold (Lines 74–75). In case the allocation fails, we expect the pointer `*pl` and the list contents to be unchanged (Lines 77–79). If it succeeds, we expect the list to be composed of the new cell followed by the old list (Lines 80–81), the old list being unchanged (Lines 82–83), and the fields of the new cell, `next` and `data`, resp., to point to the old list (Line 84) and to contain the expected value (Line 85).

## 2.2 Shape Analysis with MemCAD

The purpose of `MEMCAD` [10] is to automatically infer precise invariants about programs manipulating complex data structures. It is based on shape analysis [3], a static code analysis technique that discovers and verifies properties of recursive, dynamically allocated data structures. It relies on separation logic and abstract interpretation. Unlike in `WP`, the analysis is global.

To use `MEMCAD` on linked lists defined on Lines 1–2 of Fig. 1, the user first defines an inductive predicate expressing a structural invariant of a well-formed linked list, such as predicate `ll_cell` on Lines a–h of Fig. 2. A list, i.e. a pointer to a list cell, satisfies the predicate in two cases.
<figure><img src="image_2.png" /><figcaption>Figure 2: Inductive predicates for MEMCAD.</figcaption></figure>

<figure><img src="image_3.png" /><figcaption>Figure 3: Auxiliary MEMCAD checks for linked lists.</figcaption></figure>

Each case defines a memory separation formula and additional constraints. In the first case, the pointer is null (Line d) and no specific memory separation is required (Line c). This case has no additional arguments (cf. [0] on Line b). The second case has two (existentially quantified) arguments: an address and an integer (Line e), denoted, resp., by $0 and $1 in the rest of the case. The pointer is non null and refers to a valid memory block of 8 bytes (Line h), assuming a 32-bit system. Lines f-g define the values of the fields *next* and *data* (at offsets 0 and 4) as $0 and $1, and require separation between those fields and the rest of the list. The separation is expressed by the separating conjunction "*" [10]. Notice that "...*$0.11_cell()*..." on Line f specifies separation recursively, for all list cells reached by the predicate via the inductive case. The user can insert the instruction `_memcad("add_inductive(1,11_cell)")`; to *assume* that list 1 respects predicate `ll_cell`, or `_memcad("check_inductive(1,11_cell)")`; to *check* the same property in MEMCAD.

Predicate `cell` on Lines n-t is very close to predicate `ll_cell` except that it only defines one list cell without recursion. Predicate `plist` on Lines j-m expresses that a double pointer to a list cell (i.e. of type `list*`) is valid, refers to a well-formed list and is separated from its cells. Predicate `cell_plist` is explained below.

# 3 Combined Approach

## 3.1 Shape Analysis Assisted Verification

To prove complex memory-related annotations with WP on real-life code [11], the user typically has to manually annotate the code with many additional carefully chosen assertions establishing structural invariants and separation properties at several intermediate program points, and to add numerous lemmas to facilitate reasoning about them (whose proof must usually be done manually in COQ, an interactive proof assistant). Our approach proposes to let MEMCAD deal with the
```c
/*@                 nothing
60  assigns              \nothing;
61  ensures           \result ≠ NULL ⇒ (\valid(\result) ∧
62                        \result->next == NULL ∧ \result->data == 0); */
63 cell*  calloc_cell() {
64    cell* c = malloc(sizeof(cell));
65    if (c) { c->next = NULL; c->data = 0; }
66    return c;
67 }
/*@                 nothing
69  requires           \valid(pl);
70  requires           dptr_sep_from_list(pl, topla(*pl, NULL));
71  requires           linkedpla(*pl, NULL, topla(*pl, NULL));
72  assigns           *pl, \at(**pl, Post);
73  ensures           dptr_sep_from_list(pl, topla(*pl, NULL));
74  ensures           linkedpla(*pl, NULL, topla(*pl, NULL));
75  ensures           \result \in {0, 1};
76  ensures           \result == 0 ⇒
77                      unchangedpla{Pre, Post}(topla(*pl, NULL));
78  ensures           \result == 0 ⇒ *pl == \old(*pl);
79  ensures           \result == 1 ⇒
80                      topla(*pl, NULL) == ([|*pl|] ^ topla(\old(*pl), NULL));
81  ensures           \result == 1 ⇒
82                      unchangedpla{Pre, Post}(topla(\old(*pl), NULL));
83  ensures           \result == 1 ⇒ (*pl)->next == \old(*pl);
84  ensures           \result == 1 ⇒ (*pl)->data == data; */
85 int list_push(list* pl, int data) {
86    cell* c = calloc_cell();
87    if (!c) return 0;
88    mc_chk_sep_cell_plist(c, pl);
89    //@ admit ptr_sep_from_list(c, topla(*pl, NULL));
90    //@ admit \separated(pl, c);
91    //@ ghost Alloc:;
92    c->next = *pl;
93    //@ assert unchangedpla{Alloc,Here}(topla{Alloc}(*pl,NULL));
94    c->data = data;
95    //@ ghost Link:;
96    *pl = c;
97    //@ assert unchangedpla{Link,Here}(
98                      topla{Link}(\at(*pl,Pre),NULL));
99                      mc_chk_plist(pl);
100   //@ admit dptr_sep_from_list(pl, topla(*pl,NULL));
101   //@ admit linkedpla(*pl,NULL, topla(*pl,NULL));
102  return 1;
103 }
```

<caption>Figure 4: Functions `calloc_cell` and `list_push` with contracts.</caption>

structural invariants of recursive data structures and separation properties, and to admit them in WP at some key points.

In order to use both tools simultaneously in this way, we first need to show the equivalence between MEMCAD and WP inductive predicates. For MEMCAD, predicate `lla` (Lines a-h of Fig. 2) specifies that each element of the list is a valid cell, is separated from every other cell of the list and the list is null-terminated. This is equivalent to the `linkedll` predicate for WP (Lines 10-19 of Fig. 1) when we consider the whole list. Indeed, when `el` is `NULL`, this predicate also means that every list cell is valid and separated from any other list cell, and the list is null-terminated. Explicit separation conditions in the ACSL predicate for WP are expressed by the separating conjunction in the MEMCAD counterpart. (Notice that separation of `bl` with `NULL` on Line 15 is trivial.) The sequence of list elements, expressed by a logic list in ACSL and used to prove functional properties about the contents of the list (cf. Lines 80-81) in WP, does not need to be specified for MEMCAD, which we only use to reason about structural properties.

To check if invariants hold in MEMCAD, we define check functions shown in Fig. 3. These functions are specified to be side-effect-free (cf. Lines 40, 47) to prevent interference with the proof in WP.
The first function, `mc_chk_plist` (Lines 41–43), checks that `pl` respects the `plist` predicate, i.e. is a valid pointer to a well-formed list from which it is separated (Line 42, see also Lines j–m of Fig. 2).

The goal of the second function, `mc_chk_sep_cell_plist`, is to check that `c` refers to a list cell, `pl` respects the `plist` predicate, and the corresponding pointer and the list cells are separated from the cell referred to by `c`. To do that in MEMCAD, we introduce an ad-hoc structure `cell_plist` with both pointers (Line 45). The function initializes a local structure (Lines 49–50) and takes its address (Line 51) in order to express the required check (Line 52). This check relies on the predicate `cell_plist` (Lines v–z of Fig. 2) stating that the given pointer is non-null and refers to a structure with two pointers at offsets 0 and 4, denoted `$0` and `$1`, referring, resp., to a cell and to a double pointer to a well-formed list, which are separated (between them and from the list cells). Notice that `"...*$1.plist()"` on Line y specifies separation recursively, that is, from all locations considered in separation constraints reached via `plist` (and hence via `ll_cell`).

An important benefit of using MEMCAD is its capacity to automatically handle dynamic memory allocation, which is not yet supported in `WP`. Thus, we define a custom allocator that simulates the behavior of `calloc` for list cells on Lines 59–67 of Fig. 4. `WP` uses its contract, which is simple but currently unprovable by `WP` since dynamic allocation is not supported (it should become provable when this support is added into `WP`).

## 3.2 Proof of Function list_push

We illustrate our approach on function `list_push` of Fig. 4. It tries to allocate a new cell (Lines 87–88), and, in case of success, puts it on top of the list with the given data (Lines 93, 95, 97, 103). Lines 92, 96 define *ghost* labels (that is, labels used only in annotations).

Lines 89–91 show how we use MEMCAD to verify that the new cell (referred to by `c`) is separated both from the list cells and the pointer referred to by `pl` (Line 89), and introduce these properties as assumptions for `WP` (admit clauses on Lines 90–91). They help `WP` to prove in an `assert` clause on Line 94 that the list remains unchanged since label `Alloc` (i.e. Line 92) despite writing into the new cell on Line 93, and a similar assertion for the old list on Lines 98–99 despite the assignment on Line 97.

Instead of reasoning about the modified list directly in `WP`—which often presents another difficulty for deductive verification—we let MEMCAD check the list invariants on Line 100 and admit them on Lines 101–102 for `WP` to prove the post-conditions. Thanks to those assumptions, `WP` successfully proves this function. Notice that the check instruction for MEMCAD and the admit instructions for `WP` are placed (for the moment, manually) at the same program location to ensure the soundness of the global verification.

In order to have a full proof, we also need to run MEMCAD to verify all the checks in `list_push`. For this purpose, we define a wrapper in Fig. 5 to analyze the call to `list_push` on Line 108 with an arbitrary list respecting the given pre-conditions (which correspond in MEMCAD, as we explained above, to assuming predicate `plist` for `pl`, cf. Lines 70–72, 107). MEMCAD also succeeds in its analysis, hence, we can conclude that our function respects its ACSL contract.

While the annotation step is done manually in the current work, it can be better automated in the future. A coordinated generation of checks and assumptions for a given recursive data structure for both tools will facilitate the verification and the justification of soundness of the combined approach. An early idea consists in defining a domain-specific language for the description of the target recursive data structure that is then used for the generation of necessary predicates for MEMCAD and for `WP` as well as necessary assumptions and checks. The investigation of this research direction is left for future work.
106 int mc_verify_list_push(void) {
107 list* pl; int i; _memcad("add_inductive(pl,plist)");
108 list_push(pl, i);
109 }

<caption>Figure 5: Wrapper to verify list_push in MEMCAD.</caption>

## 4 Case study on the TPM2-TSS library

We tested our approach on a few (slightly simplified) functions of the TPM2-TSS library, a widely used open-source implementation of the TPM Software Stack (TSS)<fnref n="3" /> designed to access the Trusted Platform Module (TPM). The library uses a linked list to store and use TPM resources, such as objects sent to and received from the TPM. List cells are dynamically allocated. Simplifications were applied to data structures used for list cells (and their treatment).

We consider two functions, to add an object and to look for an object in a list, with one called function, and apply MEMCAD to verify separation properties for a newly allocated cell that WP is currently not able to deduce. A recent study [11] demonstrated that deductive verification with WP of these functions required many additional lemmas and assertions, as well as the replacement of the dynamic memory allocation by a static allocator. Interestingly, the difficulty to verify real-life code was not caused by complex operations on lists—these operations are in reality quite simple in the target code—but by the difficulty to reason about the recursive data structure itself.

The proposed approach combining deductive verification with shape analysis allows us to perform a complete proof with less effort and without replacing dynamic allocator by a static allocator. On the considered functions, the proof with WP alone [11] required 14 lemmas, leading to the generation of 241 proof obligations, one of which required a manually created WP script, and took 4m50s. Thanks to combining WP and MEMCAD in our work, we could remove ~45 auxiliary ACSL annotations and 5 lemmas, so the proof required only 9 lemmas, leading to 194 proof obligations using no scripts, and took 1min47s in total for WP and MEMCAD (the latter taking less than 1 sec.).

## 5 Related Work and Conclusion

**Related Work.** Various tools based on separation logic were proposed, such as VeriFast [8], Viper [7], VerCors [2]. He et al. [5] extract functional specification from imperative programs using a memory-safe type system and insert dynamic checks into the specification. GRASShopper [9] combines separation logic with an SMT-based verifier. Unlike in our work, GRASShopper does not integrate abstract interpretation based shape analysis (which allows us to infer structural invariants with MEMCAD without having to provide loop invariants for this tool). Issues reported in a recent study [11] motivate such combinations for complex real-life code with recursive data structures. Our work continues previous efforts by proposing a combination of weakest-precondition based deductive verification with abstract interpretation based shape analysis on the source-code level, which, to the best of our knowledge, was not studied and evaluated before.

**Conclusion and Future Work.** This short paper has presented an approach combining deductive verification with FRAMA-C/WP and shape analysis with MEMCAD. Separation properties and structural invariants for linked data structures can be more easily proved by the latter, and then used as assumptions in the former, thus allowing it to focus on other properties. This work is still ongoing and opens interesting research questions and perspectives: automation of the proposed verification technique including a coordinated generation of checks and assumptions, proof of its soundness,

<footnote n="3">³https://trustedcomputinggroup.org/work-groups/software-stack/</footnote>
design of a common (higher-level) specification mechanism for recursive data structures with automatic translation into suitable definitions for MEMCAD and FRAMA-C, as well as evaluation on other relevant case studies.

**Data-Availability Statement.** Code examples used in this paper are available online as a companion artifact on http://doi.org/10.5281/zenodo.10458675. The artifact includes a Virtual Machine containing the installed tools and code examples used, and can be used to reproduce the results of this paper.

**Acknowledgment.** Part of this work was supported by ANR (grants ANR-22-CE39-0014, ANR-22-CE25-0018) and French Ministry of Defense via a PhD grant of Yani Ziani. We thank Allan Blanchard, Laurent Corbin, Loïc Correnson, Daniel Gracia Pérez and Xavier Rival for fruitful discussions, and the anonymous referees for helpful comments.

## References

[1] Allan Blanchard, Nikolai Kosmatov, and Frédéric Louergue. Logic against ghosts: Comparison of two proof approaches for a list module. In *34th Symp. on Applied Computing, Software Verification and Testing Track (SAC-SVT'19)*, pages 2186–2195. ACM, 2019.

[2] Stefan Blom, Saeed Darabi, Marieke Huisman, and Wytse Oortwijn. The VerCors tool set: Verification of parallel and concurrent software. In *13th Int. Conf. on Integrated Formal Methods (iFM'17)*, volume 10510 of LNCS, pages 102–110. Springer, 2017.

[3] Dino Distefano, Peter W. O'Hearn, and Hongseok Yang. A local shape analysis based on separation logic. In *12th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'06)*, volume 3920 of LNCS, pages 287–302. Springer, 2006.

[4] Reiner Hähnle and Marieke Huisman. Deductive software verification: From pen-and-paper proofs to industrial tools. In *Computing and Software Science - State of the Art and Perspectives*, volume 10000 of LNCS, pages 345–373. Springer, 2019.

[5] Paul He, Eddy Westbrook, Brent Carmer, Chris Phifer, Valentin Robert, Karl Smeltzer, Andrei Stefanescu, Aaron Tomb, Adam Wick, Matthew Yacavone, and Steve Zdancewic. A type system for extracting functional specifications from memory-safe imperative programs. *Proc. ACM Program. Lang.*, 5:1–29, 2021.

[6] Florent Kirchner, Nikolai Kosmatov, Virgile Prevosto, Julien Signoles, and Boris Yakobowski. Frama-C: A software analysis perspective. *Formal Asp. Comput.*, 27(3):573–609, 2015.

[7] Peter Müller, Malte Schwerhoff, and Alexander J. Summers. Viper: A verification infrastructure for permission-based reasoning. In *17th Int. Conf. on Verification, Model Checking, and Abstract Interpretation (VMCAI'16)*, volume 9583 of LNCS, pages 41–62. Springer, 2016.

[8] Pieter Philippaerts, Jan Tobias Mühlberg, Willem Penninckx, Jan Smans, Bart Jacobs, and Frank Piessens. Software verification with VeriFast: Industrial case studies. *Science of Computer Programming*, 82:77–97, 2014.

[9] Ruzica Piskac, Thomas Wies, and Damien Zufferey. GRASShopper - complete heap verification with mixed specifications. In *20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'14)*, volume 8413 of LNCS, pages 124–139. Springer, 2014.
[10] Pascal Sotin and Xavier Rival. Hierarchical shape abstraction of dynamic structures in static blocks. In *10th Asian Symposium on Programming Languages and Systems (APLAS'12)*, volume 7705 of LNCS, pages 131-147. Springer, 2012.

[11] Yani Ziani, Nikolai Kosmatov, Frédéric Loulergue, Daniel Gracia Pérez, and Téo Bernier. Towards formal verification of a TPM software stack, 2023. URL http://arxiv.org/abs/2307.16821.