Charge!

swMATH22731MaRDI QIDQ34522FDOQ34522

Author name not available (Why is that?)

Official website: https://link.springer.com/chapter/10.1007%2F978-3-642-32347-8_21

Cited In (18)

• Mostly sound type system improves a foundational program verifier
• \textsc{Lincx}: a linear logical framework with first-class contexts
• Charge! A framework for higher-order separation logic in Coq
• HIP
• Toolchain
• VeriSmall
• TweetNaCl
• VeriML
• Backwards and forwards with separation logic
• Lincx
• Gallina
• C-to-Isabelle
• 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!