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