search

PrincetonUniversity / VST

Verified Software Toolchain
https://vst.cs.princeton.edu
Other
436 stars 92 forks source link

malloc-free #599

Closed dnaumann closed 2 years ago

dnaumann commented 2 years ago

The description for malloc-free is fine but consider embellishing slightly:

Not: Multilevel; that is, a single-layer proof directly proves high-level spec from the C program, there is no functional model in between. But there is a refinement/subsumption proof between the resource-tracking spec proved about the code and the resource-insensitive Posix-like spec used by most clients.

dnaumann commented 2 years ago

This was meant to be posted elsewhere.