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