3 ms·
Because it takes a lot of effort. Google Frama-C. On the flip side, it can express not just memory safety constraints, but also correctness proofs. In this cas
by PhilipRoman 2y ago
Because it takes a lot of effort. Google Frama-C. On the flip side, it can express not just memory safety constraints, but also correctness proofs.
In this case it's not about Frama-C or similar tools though, see your sibling comments about the caveats.
- zozbot234 2y agoArguably, generating verified C from a low-level focused subset of F* (Low*, used in the HACL project) is close enough to count as a "similar tool".