Separation and information hiding
From MaRDI portal
Recommendations
Cited in
(38)- Behaviour approximated on subgroups
- The \(\mathbf{M}\)-computations induced by accessibility relations in nonstandard models \(\mathbf{M}\) of Hoare logic
- Weak updates and separation logic
- Unifying separation logic and region logic to allow interoperability
- Fifty years of Hoare's logic
- A proof outline logic for object-oriented programming
- On assertion-based encapsulation for object invariants and simulations
- Completeness for recursive procedures in separation logic
- Certificates and Separation Logic
- Exploring an interface model for CKA
- Tackling real-life relaxed concurrency with FSL++
- A Paradigm for Masking (Camouflaging) Information
- Safe Modification of Pointer Programs in Refinement Calculus
- Abstracting Complex Data Structures by Hyperedge Replacement
- Hoare type theory, polymorphism and separation
- A semantic foundation for hidden state
- Dynamic boundaries: information hiding by second order framing with first order assertions
- Parameterised notions of computation
- An observationally complete program logic for imperative higher-order functions
- A first-order logic with frames
- Bringing Order to the Separation Logic Jungle
- Composing hidden information modules over inclusive institutions
- The dynamic frames theory
- Local reasoning for global invariants. II: Dynamic boundaries
- Separation Logic for Multiple Inheritance
- Verification of Equivalent-Results Methods
- FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
- Separation Logic Contracts for a Java-Like Language with Fork/Join
- Program Verification with Separation Logic
- Secure the clones. Static enforcement of policies for secure object copying
- Verifying pointer safety for programs with unknown calls
- Verifying programs with logic and extended proof rules: deep embedding vs. shallow embedding
- A shape graph logic and a shape system
- Juggrnaut: using graph grammars for abstracting unbounded heap structures
- Certifying low-level programs with hardware interrupts and preemptive threads
- Towards imperative modules: reasoning about invariants and sharing of mutable state
- A semantics for concurrent separation logic
- Resources, concurrency, and local reasoning
This page was built for publication: Separation and information hiding
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3452266)
