Book contents
- Frontmatter
- Dedication
- Contents
- Road map
- Acknowledgments
- 1 Introduction
- I Generic separation logic
- 2 Hoare logic
- 3 Separation logic
- 4 Soundness of Hoare logic
- 5 Mechanized Semantic Library
- 6 Separation algebras
- 7 Operators on separation algebras
- 8 First-order separation logic
- 9 A little case study
- 10 Covariant recursive predicates
- 11 Share accounting
- 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
- VII Applications
- Bibliography
- Index
2 - Hoare logic
from I - Generic separation logic
Published online by Cambridge University Press: 05 August 2014
- Frontmatter
- Dedication
- Contents
- Road map
- Acknowledgments
- 1 Introduction
- I Generic separation logic
- 2 Hoare logic
- 3 Separation logic
- 4 Soundness of Hoare logic
- 5 Mechanized Semantic Library
- 6 Separation algebras
- 7 Operators on separation algebras
- 8 First-order separation logic
- 9 A little case study
- 10 Covariant recursive predicates
- 11 Share accounting
- 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
- VII Applications
- Bibliography
- Index
Summary
- Type
- Chapter
- Information
- Program Logics for Certified Compilers , pp. 10 - 15Publisher: Cambridge University PressPrint publication year: 2014