Charge!

swMATH22731MaRDI QIDQ34522FDOQ34522

Author name not available (Why is that?)

Cited In (10)

• 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
• 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!