Program logics for certified compilers
Separation logic is the twenty-first-century variant of Hoare logic that permits verification of pointer-manipulating programs. This book covers practical and theoretical aspects of separation logic at a level accessible to beginning graduate students interested in software verification. On the prac...
| Otros Autores: | |
|---|---|
| Formato: | Libro electrónico |
| Idioma: | Inglés |
| Publicado: |
Cambridge :
Cambridge University Press
2014.
|
| Colección: | CUP ebooks.
|
| Acceso en línea: | Conectar con la versión electrónica |
| Ver en Universidad de Navarra: | https://innopac.unav.es/record=b45454929*spi |
Tabla de Contenidos:
- Generic separation logic
- Hoare logic
- Separation logic
- Soundness of Hoare logic
- Mechanized semantic library
- Separation algebras
- Operators on separation algebras
- First-order separation logic
- A little case study
- Covariant recursive predicates
- Share accounting
- Higher order separation logic
- Separation logic as a logic
- From separation algebras to separation logic
- Simplification by rewriting
- Introduction to step-indexing
- Predicate implication and subtyping
- General recursive predicates
- Case study: separation logic with first-class functions.
