Mention Heapster in the README

GaloisInc · Jun 23, 2023 · 89a80da · 89a80da
1 parent 568231e
commit 89a80da
Showing 1 changed file with 4 additions and 0 deletions.
diff --git a/CHANGES.md b/CHANGES.md
@@ -1,6 +1,10 @@
 # Version 1.0
 
 ## New Features
+* SAW now implements Heapster, which allows extracting functional specifications
+  of memory-safe C programs to Coq. There is now a family of experimental
+  `heapster_*` commands that support this. For more information, refer to the
+  [Heapster README](heapster-saw/README.md).
 
 * New commands `enable_what4_eval` and `disable_what4_eval` to enable or
   disable What4 translation for SAWCore expressions during Crucible symbolic