Linear capabilities for fully abstract compilation of separation-logic-verified code
From MaRDI portal
Recommendations
Cites work
- A verified information-flow architecture
- Abstracting gradual typing
- Featherweight VeriFast
- Formal certification of a compiler back-end or: programming a compiler with a proof assistant
- Fully abstract compilation to JavaScript
- Fully abstract compilation via universal embedding
- Fully-abstract compilation by approximate back-translation
- Gradual program verification
- Higher-order ghost state
- scientific article; zbMATH DE number 431771 (Why is no real title available?)
- Iris from the ground up: a modular foundation for higher-order concurrent separation logic
- Linear capabilities for fully abstract compilation of separation-logic-verified code
- Reasoning about a machine with local capabilities. Provably safe stack and return pointer management
- Runtime Checking for Separation Logic
- Shape Analysis for Composite Data Structures
- Sound modular verification of C code executing in an unverified context
- StkTokens: enforcing well-bracketed control flow and stack encapsulation using linear capabilities
- The essence of higher-order concurrent separation logic
- Tools and Algorithms for the Construction and Analysis of Systems
- Types and programing languages
Cited in
(5)- Sound modular verification of C code executing in an unverified context
- Shape-Value Abstraction for Verifying Linearizability
- Linear capabilities for fully abstract compilation of separation-logic-verified code
- StkTokens: enforcing well-bracketed control flow and stack encapsulation using linear capabilities
- Comparison Under Abstraction for Verifying Linearizability
This page was built for publication: Linear capabilities for fully abstract compilation of separation-logic-verified code
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5016209)
