A Formal CHERI-C Memory Model
From MaRDI portal
- A formal C memory model for separation logic
- Assessing ecosystem state space models: identifiability and estimation
- Coupled relational symbolic execution for differential privacy
- Data refinement in Isabelle/HOL
- Formal verification of C systems code. Structured types, separation logic and theorem proving
- Isabelle/HOL. A proof assistant for higher-order logic
- Light-weight containers for Isabelle: efficient, extensible, nestable
- Mechanised Separation Algebra
This page was built for software: A Formal CHERI-C Memory Model