Add summary slide about range.

[libguestfs-talks.git] / 2020-frama-c / notes.txt

diff --git a/2020-frama-c/notes.txt b/2020-frama-c/notes.txt
index 7cb905c..43dd078 100644 (file)
--- a/2020-frama-c/notes.txt
+++ b/2020-frama-c/notes.txt
@@ -402,8 +402,10 @@ point out a few things about the final proof:
    modifications, so it would be possible to maintain the annotations
    upstream, and run the proof checker as a CI test.
 
- - It probably doesn't make sense for qemu right now though, unless we
-   could prove more substantial pieces of code.
+ - It probably doesn't make sense for qemu right now though:
+   * concerted effort to prove more substantial pieces of code
+   * would need upstream effort to modularise qemu
+   * co-develop modules and proofs
 
 \f
 = POWER OF 2 =