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