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