Book contents
- Frontmatter
- Dedication
- Contents
- Road map
- Acknowledgments
- 1 Introduction
- I Generic separation logic
- II Higher order separation logic
- III Separation logic for CompCert
- 22 Verifiable C
- 23 Expressions, values, and assertions
- 24 The VST separation logic for C light
- 25 Typechecking for Verifiable C
- 26 Derived rules and proof automation for C light
- 27 Proof of a program
- 28 More C programs
- 29 Dependently typed C programs
- 30 Concurrent separation logic
- IV Operational semantics of CompCert
- V Higher-order semantic models
- VI Semantic model and soundness of Verifiable C
- VII Applications
- Bibliography
- Index
22 - Verifiable C
from III - Separation logic for CompCert
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
- 22 Verifiable C
- 23 Expressions, values, and assertions
- 24 The VST separation logic for C light
- 25 Typechecking for Verifiable C
- 26 Derived rules and proof automation for C light
- 27 Proof of a program
- 28 More C programs
- 29 Dependently typed C programs
- 30 Concurrent separation logic
- 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. 142 - 147Publisher: Cambridge University PressPrint publication year: 2014