Andrew W. AppelCambridge University Press, 4/21/2014EAN 9781107048010, ISBN10: 110704801XHardcover, 472 pages, 23.1 x 15 x 2.5 cmLanguage: EnglishSeparation 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 practical side it offers an introduction to verification in Hoare and separation logics, simple case studies for toy languages, and the Verifiable C program logic for the C programming language. On the theoretical side it presents separation algebras as models of separation logics; step-indexed models of higher-order logical features for higher-order programs; indirection theory for constructing step-indexed separation algebras; tree-shares as models for shared ownership; and the semantic construction (and soundness proof) of Verifiable C. In addition, the book covers several aspects of the CompCert verified C compiler, and its connection to foundationally verified software analysis tools. All constructions and proofs are made rigorous and accessible in the Coq developments of the open-source Verified Software Toolchain.1. IntroductionPart I. Generic Separation Logic2. Hoare logic3. Separation logic4. Soundness of Hoare logic5. Mechanized semantic library Andrew W. Appel, Robert Dockins and Aquinas Hobor6. Separation algebras7. Operators on separation algebras8. First-order separation logic9. A little case study10. Covariant recursive predicates11. Share accountingPart II. Higher-Order Separation Logic12. Separation logic as a logic13. From separation algebras to separation logic14. Simplification by rewriting15. Introduction to step-indexing16. Predicate implication and subtyping17. General recursive predicates18. Case studyseparation logic with first-class functions19. Data structures in indirection theory20. Applying higher-order separation logic21. Lifted separation logicsPart III. Separation Logic for CompCert22. Verifiable C23. Expressions, values, and assertions24. The VST separation logic for C light25. Typechecking for Verifiable C Josiah Dodds26. Derived rules and proof automation for C light27. Proof of a program28. More C programs29. Dependently typed C programs30. Concurrent separation logicPart IV. Operational Semantics of CompCert31. CompCert32. The CompCert memory model Xavier Leroy, Andrew W. Appel, Sandrine Blazy and Gordon Stewart33. How to specify a compiler Lennart Beringer, Robert Dockins and Gordon Stewart34. C light operational semanticsPart V. Higher-Order Semantic Models35. Indirection theory Aquinas Hobor, Andrew Appel and Robert Dockins36. Case studylambda-calculus with references37. Higher-order Hoare logic38. Higher-order separation logic39. Semantic models of predicates-in-the-heapPart VI. Semantic Model and Soundness of Verifiable C40. Separation algebra for CompCert41. Share models42. Juicy memories Gordon Stewart and Andrew W. Appel43. Modeling the Hoare judgment44. Semantic model of CSL45. Modular structure of the developmentPart VII. Applications46. Foundational static analysis47. Heap theorem prover Gordon Stewart, Lennart Beringer and Andrew W. Appel.
