Cited in
(13)- Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs
- Verified characteristic formulae for CakeML
- Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits
- ModuRes
- TweetNaCl
- HALO
- Grail
- CertiCoq
- Charge!
- Camelot
- VST-Floyd
- VST-Floyd: a separation logic tool to verify correctness of C programs
- On models of higher-order separation logic
This page was built for software: Bedrock
