sepviz-software-foundations-slf/Postscript.v at viz · epfl-systemf/sepviz-software-foundations-slf · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
(** * Postscript: Conclusion and Perspectives *)

(* ################################################################# *)
(** * Beyond the Scope of This Course *)

(** This course has focused on the foundations of Separation Logic for
    sequential programs, and discussed the set up of tooling for computing
    weakest preconditions.

    There are numerous aspects of Separation Logic that were not covered in this
    course, including:

    - Concurrent Separation Logic, for reasoning about concurrent programs.
    - Automated reasoning using Separation Logic, typically for a restricted
      fragment of Separation Logic.
    - Separation Logic for low-level programs, at the byte level, and with
      assembly-style code written in continuation-passing style.
    - Separation Logic for object-oriented programs.
    - Reasoning about I/O, integer overflows, floatting-point arithmetics,
      etc. *)

(* ################################################################# *)
(** * Tools Leveraging Separation Logic *)

(** Ideas of Separation Logic have had significant influence on the field of
    programming languages from various perspectives. For a broad survey of
    Separation Logic, we refer to Peter O'Hearn's CACM paper [2019].
    https://dl.acm.org/doi/10.1145/3211968 (Make sure to also download the
    "supplementary material" link at the bottom of the page.)

    Here is a non-exhaustive list of active projects leveraging Separation
    Logic.

    - The tool "Infer" leverages for static analysis, that is, fully automated
      program analysis to produce a list of potential bugs.
      https://fbinfer.com/
      https://fbinfer.com/docs/separation-logic-and-bi-abduction/

    - The programming language "Rust" features a type system with "borrows", a
      notion directly inspired by Separation Logic.

    - The tool "VeriFast" targets C and Java programs.
      https://people.cs.kuleuven.be/~bart.jacobs/verifast and
      https://github.com/verifast/verifast

    - The tool "Verifiable C" tool, from the VST project, targets the
      verification of C code, using interactive Rocq proofs based on Separation
      Logic.
      https://vst.cs.princeton.edu/
      See also volume 5 of Software Foundations.

    - The tool "Viper" is based on a variant of Separation Logic, its front-end
      supports several languages, and its backend leverages the SMT solver Z3;
      it also supports user annotations in the code for guiding proofs.
      https://www.pm.inf.ethz.ch/research/viper.html

    - The "Isabelle Refinement Framework" leverages Separation Logic is the
      process of refining monadic high-order logic definitions into efficient
      imperative code. It can be used to produce verified ML code, as well as
      LLVM IR code.
      https://www21.in.tum.de/~lammich/pub/itp15_sepref.pdf

    - The tool "CFML" targets the verification of OCaml programs. The original
      version of CFML leverages a version of characteristic formulae slightly
      more complicated than the one presented in this volume. The new version,
      CFML 2.0, directly leverages all the ideas from this course, in particular
      the weakest-precondition style [wpgen] function.

    - The verified compiler "CakeML" implements technology similar to that
      of CFML, and leverages it to verify components from its standard library
      and from its runtime.

    - The Iris project develops advanced logics for reasoning about concurrent
      programs using Separation Logic. *)

(* ################################################################# *)
(** * Related Courses *)

(** The following courses focus on reasoning about programs, and should be of
    interest to the reader:

    - Verifiable C, volume 5 of Sofware Foundations, by Andrew Appel.
      https://softwarefoundations.cis.upenn.edu/vc-current/index.html

    - Formal Reasoning About Programs, by Adam Chlipala.
      http://adam.chlipala.net/frap/

    - The Iris tutorial, by Birkedal and Bizjak, presents the core ideas of
      Iris' concurrent Separation Logic.
      https://iris-project.org/tutorial-material.html

*)

(* ################################################################# *)
(** * Acknowledgments *)

(** The lead author of this volume, Arthur Charguéraud, wishes to thank:

    - Benjamin Pierce, for demonstrating the benefits of Rocq-based teaching,
      for coordinating the Software Foundations series, and for encouraging
      me to write this volume.
    - The Software Foundations (SF) community, for helping to polish the course
      material and the tooling, and contributing to the success of teaching
      using this material.
    - François Pottier, with whom I developed several extensions of Separation
      Logic, and thereby obtained a deeper understanding of this logic.
    - Jacques-Henri Jourdan, who introduced me to a number of techniques used
      in the Iris project, and contributed to the definition of [mkstruct].
    - Xavier Leroy, with whom I had numerous discussions on mechanized
      semantics.
    - Jean-Christophe Filliâtre, for numerous discussions on program
      verification.
    - Andrew Appel, Lars Birkedal, Adam Chlipala, Magnus Myreen, Gerwin Klein,
      Peter Lammich, and Zhong Shao, who kindly answered questions on related
      work aspects.
    - The many readers who helped fixing typos.

*)

(* 2026-01-07 13:36 *)