Cited in
(18)- Mostly sound type system improves a foundational program verifier
- \textsc{Lincx}: a linear logical framework with first-class contexts
- HIP
- Toolchain
- VeriSmall
- TweetNaCl
- VeriML
- Lincx
- Gallina
- C-to-Isabelle
- Charge! A framework for higher-order separation logic in Coq
- Backwards and forwards with separation logic
- Temporary read-only permissions for separation logic
- A relational shape abstract domain
- Formally verifying exceptions for low-level code with separation logic
- Featherweight VeriFast
- VST-Floyd: a separation logic tool to verify correctness of C programs
- Extensible and efficient automation through reflective tactics
This page was built for software: Charge!
