Book contents
- Frontmatter
- Dedication
- Contents
- Road map
- Acknowledgments
- 1 Introduction
- I Generic separation logic
- II Higher order separation logic
- III Separation logic for CompCert
- IV Operational semantics of CompCert
- V Higher-order semantic models
- VI Semantic model and soundness of Verifiable C
- 40 Separation algebra for CompCert
- 41 Share models
- 42 Juicy memories
- 43 Modeling the Hoare judgment
- 44 Semantic model of CSL
- 45 Modular structure of the development
- VII Applications
- Bibliography
- Index
43 - Modeling the Hoare judgment
from VI - Semantic model and soundness of Verifiable C
Published online by Cambridge University Press: 05 August 2014
- Frontmatter
- Dedication
- Contents
- Road map
- Acknowledgments
- 1 Introduction
- I Generic separation logic
- II Higher order separation logic
- III Separation logic for CompCert
- IV Operational semantics of CompCert
- V Higher-order semantic models
- VI Semantic model and soundness of Verifiable C
- 40 Separation algebra for CompCert
- 41 Share models
- 42 Juicy memories
- 43 Modeling the Hoare judgment
- 44 Semantic model of CSL
- 45 Modular structure of the development
- VII Applications
- Bibliography
- Index
Summary
- Type
- Chapter
- Information
- Program Logics for Certified Compilers , pp. 392 - 400Publisher: Cambridge University PressPrint publication year: 2014